Complexity of solvable cases of the decision problem for the predicate calculus
- 1 October 1978
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 02725428,p. 35-47
- https://doi.org/10.1109/sfcs.1978.9
Abstract
We analyze the computational complexity of determining whether F is satisfiable when F is a formula of the classical predicate calculus which obeys certain syntactic restrictions. For example, for the monadic predicate calculus and the Gödel or ∃ ... ∃∀∀∃ ... ∃ prefix class we obtain lower and upper nondeterministic time bounds of the form cn/log n. The main tool in in these proofs is a finite version of Wang's domino problem, about which we present an interesting open question.Keywords
This publication has 12 references indexed in Scilit:
- Elementary bounds for presburger arithmeticPublished by Association for Computing Machinery (ACM) ,1973
- Turing machines and the spectra of first-order formulas with equalityPublished by Association for Computing Machinery (ACM) ,1972
- The complexity of theorem-proving proceduresPublished by Association for Computing Machinery (ACM) ,1971
- The undecidability of the domino problemMemoirs of the American Mathematical Society, 1966
- Turing-machines and the EntscheidungsproblemMathematische Annalen, 1962
- Untersuchungen zum Entscheidungsproblem der mathematischen LogikMathematische Annalen, 1934
- Über die Erfüllbarkeit derjenigen Zählausdrücke, welche in der Normalform zwei benachbarte Allzeichen enthaltenMathematische Annalen, 1933
- Über die Erfüllbarkeit gewisser ZählausdrückeMathematische Annalen, 1928
- Zum Entscheidungsproblem der mathematischen LogikMathematische Annalen, 1928
- Über Möglichkeiten im RelativkalkülMathematische Annalen, 1915