6533b820fe1ef96bd1279180

RESEARCH PRODUCT

Logics with counting and equivalence

Ian Pratt-hartmann

subject

Discrete mathematicsLogical equivalenceComplexityHigher-order logicSatisfiabilityUndecidable problemStipulationCombinatoricsBinary predicateTheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESEquivalence relationComputer Science::Logic in Computer ScienceEquivalence relationSatisfiabilityEquivalence (formal languages)Mathematics

description

We consider the two-variable fragment of first-order logic with counting, subject to the stipulation that a single distinguished binary predicate be interpreted as an equivalence. We show that the satisfiability and finite satisfiability problems for this logic are both NEXPTIME-complete. We further show that the corresponding problems for two-variable first-order logic with counting and two equivalences are both undecidable.

yearjournalcountryeditionlanguage
2014-07-14Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
https://doi.org/10.1145/2603088.2603117