• Two variable first-order logic...

Treffer: Two variable first-order logic over ordered domains

Title:
Two variable first-order logic over ordered domains
Authors:
Martin Otto
Source:
Journal of Symbolic Logic. 66:685-702
Publisher Information:
Cambridge University Press (CUP), 2001.
Publication Year:
2001
Subject Terms:
Complexity of computation (including implicit computational complexity), Analysis of algorithms and problem complexity, satisfiability problem, finite satisfiability, decidability, complexity of decision problems, 0102 computer and information sciences, 16. Peace & justice, 01 natural sciences, Decidability of theories and sets of sentences, undecidability, computation tree logic, 0101 mathematics, Subsystems of classical logic (including intuitionistic logic), two-variable fragment of first-order logic
Document Type:
Fachzeitschrift Article
File Description:
application/xml
Language:
English
ISSN:
1943-5886
0022-4812
DOI:
10.2307/2695037
Access URL:
https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/two-variable-firstorder-logic-over-ordered-domains/FFDCCC2DD9896C1715D2A77534BC840C
https://projecteuclid.org/euclid.jsl/1183746466
https://dblp.uni-trier.de/db/journals/jsyml/jsyml66.html#Otto01
Rights:
Cambridge Core User Agreement
Accession Number:
edsair.doi.dedup.....4ba61c7b51aaff5d33753d9a8a464a38
Database:
OpenAIRE

Weitere Informationen

The satisfiability problem for the two-variable fragment of first-order logic is investigated over finite and infinite linearly ordered, respectively wellordered domains, as well as over finite and infinite domains in which one or several designated binary predicates are interpreted as arbitrary wellfounded relations.It is shown that FO2 over ordered, respectively wellordered. domains or in the presence of one well-founded relation, is decidable for satisfiability as well as for finite satisfiability. Actually the complexity of these decision problems is essentially the same as for plain unconstrained FO2. namely non-deterministic exponential time.In contrast FO2 becomes undecidable for satisfiability and for finite satisfiability, if a sufficiently large number of predicates are required to be interpreted as orderings. wellorderings. or as arbitrary wellfounded relations. This undecidability result also entails the undecidability of the natural common extension of FO2 and computation tree logic CTL.