manuscripta mathematica

, Volume 22, Issue 1, pp 13–25 | Cite as

Das Entscheidungsproblem der Klasse von Formeln, die höchstens zwei Primformeln enthalten

  • Martin Wirsing


For classes of formulas containing at most two atomic sub-formulas the decision problem of first-order predicate logic with identity and function variables is treated. The class of all formulas of the form Q (α ∨ β), where Q is prefix and α, β are atomic formulas or negated atomic formulas, is decidable with respect to satisfiability. The class of all formulas of the form ∀x1...∀x6(α ∨ β) is a conservative reduction class and therefore is undecidable.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Börger,E.: Reduktionstypen in Krom- und Hornformeln. Dissertation Münster 1971.Google Scholar
  2. [2]
    Börger,E.: Eine einfache Methode zur Bestimmung der Unlösbarkeitsgrade von Entscheidungsproblemen kombinatori-scher Systeme. Habilitationsschrift Münster 1975.Google Scholar
  3. [3]
    Börger,E.,Heidler,K.: Die m-Grade logischer Entscheidungsprobleme. Arch.math.Logik 17, 105–112 (1976).Google Scholar
  4. [4]
    Gladstone,M.D.: Finite models for inequations. JSL 31 581–592 (1966).Google Scholar
  5. [5]
    Gurevic,J.S.: Semi-conservative reduction and decision problem for standard classes. Techn. Report Ben Gurion University 1974.Google Scholar
  6. [6]
    Gurevic,J.S.: Semi-conservative reduction. Arch.math. Logik 18, 23–25 (1976)Google Scholar
  7. [7]
    Lewis,H.R., Goldfarb,W.D.: The decision problem for formulas with a small number of atomic subformulas. JSL 38, 471–480 (1973).Google Scholar
  8. [8]
    Minsky,M.L.: Recursive unsolvability of Post's problem of “Tag” and other topics in theory of Turing machines. Annals of Math. 74, 437–455 (1961).Google Scholar
  9. [9]
    Minsky,M.L.: Computation: Finite and infinite machines. Prentice-Hall, Englewood Cliffs 1967.Google Scholar
  10. [10]
    McNulty,G.F.: Undecidable properties of finite sets of equations. JSL 41, 589–604 (1976).Google Scholar
  11. [11]
    Rogers,H.,Jr.: Theory of recursive functions and effective computability. McGraw-Hill, New York 1967.Google Scholar
  12. [12]
    Tarski,A.: Equational logic. Contributions to mathematical logic (ed. by K. Schütte), North-Holland, Amsterdam 1968, 275–288.Google Scholar
  13. [13]
    Wirsing,M.: Das Entscheidungsproblem der Prädikatenlogik 1.Stufe mit Identität und Funktionszeichen in Herbrandformeln. Dissertation Universität München 1976.Google Scholar
  14. [14]
    Wirsing,M.: Probléme de décision du calcul des prédicats avec egalité et symboles fonctionels: formules de Herbrand. Résumé dans JSL 4?(197?).Google Scholar

Copyright information

© Springer-Verlag 1977

Authors and Affiliations

  • Martin Wirsing
    • 1
  1. 1.Institut für Informatik der Technischen UniversitätMünchen 2Bundesrepublik Deutschland

Personalised recommendations