Abstract
We consider the complexity of deciding satisfiability of formulas in full first order logic (including function symbols and equality) which obey restrictions on their quantifier prefix and their relation and function symbols (prefix vocabulary classes). This extends results of H. Lewis and M.Fürer on the complexity of the classical solvable cases of the decision problem.
We obtain complexity results for the maximal solvable cases and some of their subcases. In particular we give a complete classification of the prefix vocabulary classes in P and in NP.
Address after fall 1989: Mathematisches Institut der Universität Basel, Rheinsprung 21, CH-4051 Basel, Switzerland; e-mail: graedel@urz.unibas.ch. This work was supported by the Swiss National Science Foundation.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
W. Ackermann, Über die Erfüllbarkeit gewisser Zählausdrücke, Math. Annalen 100 (1928), 638–649.
P. Bernays and M. Schönfinkel, Zum Entscheidungsproblem der mathematischen Logik, Math. Annalen 99 (1928), 342–372.
E. Börger, Decision problems in predicate logic, in: “Logic Colloquium 82”, Elsevier (North Holland) 1984, 263–301.
K. Compton and C. W. Henson, A uniform method for proving lower bounds on the computational complexity of logical theories, to appear in Annals of Pure and Applied Logic.
B. Dreben and W. Goldfarb, The decision problem, Addison-Wesley, Reading (MA) 1979.
M. Fürer, Alternation and the Ackermann case of the decision problem, in: “Logic and Algorithmic”, Monographie Nr. 30 de L'Enseignement Mathématique, Genève 1982, 161–186.
K. Gödel, Ein Spezialfall des Entscheidungsproblems der theoretischen Logik, Ergebnisse eines mathematischen Kolloquiums 2 (1932), 27–28.
W. Goldfarb, The unsolvability of the Gödel class with identity, J. Symbolic Logic 49 (1984), 1237–1252.
E. Grädel, Satisfiability of formulas with one ∀ is decidable in exponential time, submitted for publication.
Y. Gurevich, Ob effektivnom rasponznavanii vipolnimosti formul UIP, Algebra i Logika 5 (1966), 25–55 (in Russian).
Y. Gurevich, The decision problem for the logic of predicates and operations, Algebra and Logic 8 (1969), 294–308.
Y. Gurevich, Formuly s odnim ∀ (Formulas with one ∀), in: “Izbrannye voprosy algebry i logiki”, (Selected Questions in Algebra and Logic; in memory of A. Malćev), Nauka, Novosibirsk 1973, 97–110 (in Russian).
Y. Gurevich, The decision problem for standard classes, J. Symbolic Logic 41 (1976), 460–464.
A. Kahr, E. Moore and H. Wang, Entscheidungsproblem reduced to the ∀∃∀ case, Proc. Nat. Acad. Sci. U.S.A. 48 (1962), 365–377.
P. Kolaitis and M. Vardi, 0–1 Laws and Decision Problems for Fragments of Second-Order Logic, Proceedings of 3rd IEEE Symposium on Logic in Computer Science 1988, 2–11.
H. Lewis, Unsolvable Classes of Quantificational Formulas, Addison Wesley, Reading (MA) 1979.
H. Lewis, Complexity Results for Classes of Quantificational Formulas, J. of Computer and System Sciences 21 (1980), 317–353.
L. Löwenheim, Über Möglichkeiten im Relativkalkül, Math. Annalen 76 (1915), 447–470.
A. Meyer, The inherent computational complexity of theories of ordered sets, in: “Proc. 1974 Int. Cong. of Mathematicians”, Vancouver (1974), 477–482.
S. Shelah, Decidability of a portion of the predicate calculus, Israel J. Math 28 (1977), 32–44.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grädel, E. (1989). Complexity of formula classes in first order logic with functions. In: Csirik, J., Demetrovics, J., Gécseg, F. (eds) Fundamentals of Computation Theory. FCT 1989. Lecture Notes in Computer Science, vol 380. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-51498-8_21
Download citation
DOI: https://doi.org/10.1007/3-540-51498-8_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-51498-5
Online ISBN: 978-3-540-48180-5
eBook Packages: Springer Book Archive