Term satisfiability in FL_ew-algebras

详细信息    查看全文

• 作者：Zuzana Haniková ; ; ^{hanikova@cs.cas.cz" class="auth_mail" title="E-mail the corresponding author} ; Petr Savický ; ^{savicky@cs.cas.cz" class="auth_mail" title="E-mail the corresponding author}
• 关键词：Substructural logic ; FLewFLew-algebra ; MV-algebra ; Satisfiability ; Computational complexity
• 刊名：Theoretical Computer Science
• 出版年：2016
• 出版时间：6 June 2016
• 年：2016
• 卷：631
• 期：Complete
• 页码：1-15
• 全文大小：484 K

文摘

class="mathmlsrc">class="formulatext stixSupport mathImg" data-mathURL="/science?_ob=MathURL&_method=retrieve&_eid=1-s2.0-S0304397516001997&_mathId=si1.gif&_user=111111111&_pii=S0304397516001997&_rdoc=1&_issn=03043975&md5=d6c872fb3967f4daf4cc72fbdb97cbce" title="Click to view the MathML source">FL_ewclass="mathContainer hidden">class="mathCode">${\mathrm{FL}}_{\mathrm{ew}}$-algebras form the algebraic semantics of the full Lambek calculus with exchange and weakening. We investigate two relations, called satisfiability and positive satisfiability  , between class="mathmlsrc">class="formulatext stixSupport mathImg" data-mathURL="/science?_ob=MathURL&_method=retrieve&_eid=1-s2.0-S0304397516001997&_mathId=si1.gif&_user=111111111&_pii=S0304397516001997&_rdoc=1&_issn=03043975&md5=d6c872fb3967f4daf4cc72fbdb97cbce" title="Click to view the MathML source">FL_ewclass="mathContainer hidden">class="mathCode">${\mathrm{FL}}_{\mathrm{ew}}$-terms and class="mathmlsrc">class="formulatext stixSupport mathImg" data-mathURL="/science?_ob=MathURL&_method=retrieve&_eid=1-s2.0-S0304397516001997&_mathId=si1.gif&_user=111111111&_pii=S0304397516001997&_rdoc=1&_issn=03043975&md5=d6c872fb3967f4daf4cc72fbdb97cbce" title="Click to view the MathML source">FL_ewclass="mathContainer hidden">class="mathCode">${\mathrm{FL}}_{\mathrm{ew}}$-algebras. For each class="mathmlsrc">class="formulatext stixSupport mathImg" data-mathURL="/science?_ob=MathURL&_method=retrieve&_eid=1-s2.0-S0304397516001997&_mathId=si1.gif&_user=111111111&_pii=S0304397516001997&_rdoc=1&_issn=03043975&md5=d6c872fb3967f4daf4cc72fbdb97cbce" title="Click to view the MathML source">FL_ewclass="mathContainer hidden">class="mathCode">${\mathrm{FL}}_{\mathrm{ew}}$-algebra, the sets of its satisfiable and positively satisfiable terms can be viewed as fragments of its existential theory; we identify and investigate the complements as fragments of its universal theory. We offer characterizations of those algebras that (positively) satisfy just those terms that are satisfiable in the two-element Boolean algebra providing its semantics to classical propositional logic. In case of positive satisfiability, these algebras are just the nontrivial weakly contractive class="mathmlsrc">class="formulatext stixSupport mathImg" data-mathURL="/science?_ob=MathURL&_method=retrieve&_eid=1-s2.0-S0304397516001997&_mathId=si1.gif&_user=111111111&_pii=S0304397516001997&_rdoc=1&_issn=03043975&md5=d6c872fb3967f4daf4cc72fbdb97cbce" title="Click to view the MathML source">FL_ewclass="mathContainer hidden">class="mathCode">${\mathrm{FL}}_{\mathrm{ew}}$-algebras. In case of satisfiability, we give a characterization by means of another property of the algebra, the existence of a two-element congruence. Further, we argue that (positive) satisfiability problems in class="mathmlsrc">class="formulatext stixSupport mathImg" data-mathURL="/science?_ob=MathURL&_method=retrieve&_eid=1-s2.0-S0304397516001997&_mathId=si1.gif&_user=111111111&_pii=S0304397516001997&_rdoc=1&_issn=03043975&md5=d6c872fb3967f4daf4cc72fbdb97cbce" title="Click to view the MathML source">FL_ewclass="mathContainer hidden">class="mathCode">${\mathrm{FL}}_{\mathrm{ew}}$-algebras are computationally hard. Some previous results in the area of term satisfiability in MV-algebras or BL-algebras are thus brought to a common footing with known facts on satisfiability in Heyting algebras.