6533b7dcfe1ef96bd127358c

RESEARCH PRODUCT

Equivalence closure in the two-variable guarded fragment

Ian Pratt-hartmannLidia TenderaEmanuel Kieronski

subject

Computational complexity theoryLogiccomputational complexityguarded fragmentsatisfiability problemBinary numberTheoretical Computer ScienceCombinatoricsArts and Humanities (miscellaneous)Computer Science::Logic in Computer ScienceClosure operatorEquivalence (formal languages)MathematicsDiscrete mathematicssatisfiability problemcomputational complexitydecidabilityequivalence closureSatisfiabilityDecidabilityTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESClosure (computer programming)Hardware and ArchitectureTheoryofComputation_LOGICSANDMEANINGSOFPROGRAMSBoolean satisfiability problemSoftware

description

We consider the satisfiability and finite satisfiability problems for the extension of the two-variable guarded fragment in which an equivalence closure operator can be applied to two distinguished binary predicates. We show that the satisfiability and finite satisfiability problems for this logic are 2-ExpTime-complete. This contrasts with an earlier result that the corresponding problems for the full two-variable logic with equivalence closures of two binary predicates are 2-NExpTime-complete.

yearjournalcountryeditionlanguage
2015-12-04Journal of Logic and Computation
https://doi.org/10.1093/logcom/exv075