Skip to main content
SpringerLink
Log in

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

  • Published:
manuscripta mathematica Aims and scope Submit manuscript

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Literatur

  1. Börger,E.: Reduktionstypen in Krom- und Hornformeln. Dissertation Münster 1971.

  2. Börger,E.: Eine einfache Methode zur Bestimmung der Unlösbarkeitsgrade von Entscheidungsproblemen kombinatori-scher Systeme. Habilitationsschrift Münster 1975.

  3. Börger,E.,Heidler,K.: Die m-Grade logischer Entscheidungsprobleme. Arch.math.Logik 17, 105–112 (1976).

    Google Scholar 

  4. Gladstone,M.D.: Finite models for inequations. JSL 31 581–592 (1966).

    Google Scholar 

  5. Gurevic,J.S.: Semi-conservative reduction and decision problem for standard classes. Techn. Report Ben Gurion University 1974.

  6. Gurevic,J.S.: Semi-conservative reduction. Arch.math. Logik 18, 23–25 (1976)

    Google Scholar 

  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. 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. Minsky,M.L.: Computation: Finite and infinite machines. Prentice-Hall, Englewood Cliffs 1967.

    Google Scholar 

  10. McNulty,G.F.: Undecidable properties of finite sets of equations. JSL 41, 589–604 (1976).

    Google Scholar 

  11. Rogers,H.,Jr.: Theory of recursive functions and effective computability. McGraw-Hill, New York 1967.

    Google Scholar 

  12. Tarski,A.: Equational logic. Contributions to mathematical logic (ed. by K. Schütte), North-Holland, Amsterdam 1968, 275–288.

    Google Scholar 

  13. Wirsing,M.: Das Entscheidungsproblem der Prädikatenlogik 1.Stufe mit Identität und Funktionszeichen in Herbrandformeln. Dissertation Universität München 1976.

  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?).

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik der Technischen Universität, Arcisstr. 21, D-8000, München 2, Bundesrepublik Deutschland

    Martin Wirsing

Authors
  1. Martin Wirsing
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

Dieser Aufsatz beruht auf Resultaten der Dissertation [13], die der Universität München im Sommersemester 1976 vorgelegt wurde.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Wirsing, M. Das Entscheidungsproblem der Klasse von Formeln, die höchstens zwei Primformeln enthalten. Manuscripta Math 22, 13–25 (1977). https://doi.org/10.1007/BF01182063

Download citation

  • Received:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF01182063

Search

Navigation