Journal article icon

Journal article

Complexity of two-variable logic on finite trees

Abstract:

Verification of properties expressed in the two-variable fragment of first-order logic FO2 has been investigated in a number of contexts. The satisfiability problem for FO2 over arbitrary structures is known to be NEXPTIME-complete, with satisfiable formulas having exponential-sized models. Over words, where FO2 is known to have the same expressiveness as unary temporal logic, satisfiability is again NEXPTIME-complete. Over finite labelled ordered trees, FO2 has the same expressiveness as nav...

Expand abstract
Publication status:
Published
Peer review status:
Peer reviewed
Version:
Accepted Manuscript

Actions


Access Document


Files:
Publisher copy:
10.1145/2996796

Authors


More by this author
Department:
Oxford, MPLS, Computer Science
More by this author
Department:
University College
Charatonik, W More by this author
Kieroński, E More by this author
More by this author
Department:
Oxford, MPLS, Computer Science
Expand authors...
Publisher:
Association for Computing Machinery Publisher's website
Journal:
ACM Transactions on Computational Logic Journal website
Volume:
17
Issue:
4
Pages:
1-38
Publication date:
2016-11-01
Acceptance date:
2016-09-01
DOI:
EISSN:
1557-945X
ISSN:
1529-3785
Pubs id:
pubs:664491
URN:
uri:4a8207dd-6dad-4a13-a4cf-82ad51f6e822
UUID:
uuid:4a8207dd-6dad-4a13-a4cf-82ad51f6e822
Local pid:
pubs:664491
Keywords:

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP