Hostname: page-component-586b7cd67f-t8hqh Total loading time: 0 Render date: 2024-11-28T01:35:20.706Z Has data issue: false hasContentIssue false
  • English
  • Français

Conservative reduction classes of Krom formulas1

Published online by Cambridge University Press:  12 March 2014

Stål O. Aanderaa ,
Egon Börger  and
Harry R. Lewis
Stål O. Aanderaa
Affiliation:
University of Oslo, Blindern, Oslo 3, Norway
Egon Börger
Affiliation:
Universität Dortmund, 46 Dortmund 50, Federal Republic of, Germany
Harry R. Lewis
Affiliation:
Harvard University, Cambridge, Massachusetts 02138
Get access Rights & Permissions [Opens in a new window]

Abstract

A Krom formula of pure quantification theory is a formula in conjunctive normal form such that each conjunct is a disjunction of at most two atomic formulas or negations of atomic formulas. Every class of Krom formulas that is determined by the form of their quantifier prefixes and which is known to have an unsolvable decision problem for satisfiability is here shown to be a conservative reduction class. Therefore both the general satisfiability problem, and the problem of satisfiability in finite models, can be effectively reduced from arbitrary formulas to Krom formulas of these several prefix types.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 47 , Issue 1 , March 1982 , pp. 110 - 130
Copyright
Copyright © Association for Symbolic Logic 1982

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

1

The authors thank the “Stiftung Volkswagenwerk” for its financial support of the conference on logic and complexity theory held in Aachen in September 1979, during which this collaborative work was initiated, and also the Institut für Mathematische Logik und Grundlagenforschung of the University of Münster for its hospitality during the week after the conference. We are also grateful to Warren Goldfarb for his corrections to an earlier draft of this paper.

References

REFERENCES

[A]Aanderaa, S. O., On the decision problem for formulas in which all disjunctions are binary, Proceedings of the Second Scandinavian Logic Symposium, North-Holland, Amsterdam, 1971, pp. 1–18.Google Scholar
[ABG]Aanderaa, S. O., Börger, E. and Gurevich, Y., Prefix classes of Kromformulae with identity, Archiv für Mathematische Logik und Grundlagenforschung (to appear).Google Scholar
[AL]Aanderaa, S. O. and Lewis, H. R., Prefix classes of Krom formulas, this Journal, vol. 38 (1973), pp. 628–642.Google Scholar
[B1]Börger, E., Reduktionstypen in Krom- und Hornformeln, Inauguraldissertation, Westfälische Wilhelms-Universität, Münster, 1971.Google Scholar
[B2]Börger, E., Reduktionstypen der klassischen Prädikatenlogik, unpublished lecture notes, Westfälische Wilhelms-Universität, Münster, 1972.Google Scholar
[DG]Dreben, B. and Goldfarb, W. D., The decision problem: Solvable classes of quantificational formulas, Addision-Wesley, Reading, Massachusetts, 1979.Google Scholar
[Gu]Gurevich, Y., Semi-conservative reduction, Archiv für Mathematische Logik, vol. 18 (1976), pp. 23–25.CrossRefGoogle Scholar
[K1]Krom, M. R., The decision problem for a class of first-order formulas in which all disjunctions are binary, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 13 (1967), pp. 15–20.CrossRefGoogle Scholar
[K2]Krom, M. R., The decision problem for formulas in prenex conjunctive normal form with binary disjunctions, this Journal, vol. 35 (1970), pp. 210–216.Google Scholar
[L]Lewis, H. R., Unsolvable classes of quantificational formulas, Addison-Wesley, Reading, Massachusetts, 1979.Google Scholar
[LG]Lewis, H. R. and Goldfarb, W. D., The decision problem for formulas with a small number of atomic subformulas, this Journal, vol. 38 (1973), pp. 471–480.Google Scholar
[Ma]Maslov, S. Yu., Obratniy metod ystanovleniya vyvodimosti v klassicheskom ischislenii predikatov, Doklady Akademii Nauk SSSR, vol. 159 (1964), pp. 17–20; English translation in Soviet Mathematics-Doklady, vol. 5 (1964), pp. 1420–1424.Google Scholar
[Mi]Minsky, M., Computation: finite and infinite machines, Prentice-Hall, Englewood Cliffs, New Jersey, 1967.Google Scholar
[T1]Trakhtenbrot, B. A., Nevozmozhnost' algorifma dlya problemy razreshimosti na konechnykh klassakh, Doklady Akademii Nauk SSSR, vol. 70 (1950), pp. 569–572; translation in American Mathematical Society Translations (2), vol. 23 (1963), pp. 1–5.Google Scholar
[T2]Trakhtenbrot, B. A., O rekursivnoi otdyelimosti, Doklady Akademii Nauk SSSR, vol. 88 (1953), pp. 953–955.Google Scholar