Logics with Counting and Equivalence

Ian Pratt-Hartmann, Thomas Henzinger (Editor), Dale Miller (Editor)

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Abstract

    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.
    Original languageEnglish
    Title of host publicationACM/IEEE Symposium on Logic in Computer Science
    EditorsThomas Henzinger, Dale Miller
    PublisherAssociation for Computing Machinery
    Pages1-10
    Number of pages10
    ISBN (Print)978-1-4503-2886-9
    DOIs
    Publication statusPublished - 12 Jul 2014
    EventCSL-LICS '14 Proceedings 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) - Vienna
    Duration: 12 Jul 201424 Jul 2014

    Conference

    ConferenceCSL-LICS '14 Proceedings 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)
    CityVienna
    Period12/07/1424/07/14

    Keywords

    • Equivalence relation
    • Satisfiability
    • Complexity

    Fingerprint

    Dive into the research topics of 'Logics with Counting and Equivalence'. Together they form a unique fingerprint.

    Cite this