Hostname: page-component-78c5997874-dh8gc Total loading time: 0 Render date: 2024-11-16T15:24:20.690Z Has data issue: false hasContentIssue false
  • English
  • Français

Krom formulas with one dyadic predicate letter1

Published online by Cambridge University Press:  12 March 2014

Harry R. Lewis
Harry R. Lewis*
Affiliation:
Harvard University, Cambridge, Massachusetts 02138
Get access Rights & Permissions [Opens in a new window]

Extract

Let Kr be the class of all those quantificational formulas whose matrices are conjunctions of binary disjunctions of signed atomic formulas. Decision problems for subclasses of Kr do not invariably coincide with those for the corresponding classes of quantificational formulas with unrestricted matrices; for example, the ∀∃∀ prefix subclass of Kr is solvable, but the full ∀∃∀ class is not ([AaLe],- [KMW]). Moreover, the straightforward encodings of automata which have been used to show the unsolvability of various subclasses of Kr ([Aa], [Bö], [AaLe]) yield but little information about signature subclasses, i.e. subclasses determined by the number and degrees of the predicate letters occurring in a formula. By a new and highly complex construction Theorem 1 establishes the best possible result on classification by signature.

Theorem 1. Let C be the class of all formulas in Kr with a single predicate letter, which is dyadic; then C is a reduction class for satisfiability.

Thus a signature subclass of Kr is solvable just in case the corresponding class of unrestricted quantificational formulas is solvable, to wit, just in case no predicate letter of degree exceeding one may occur. To obtain a richer classification by signature we consider further restrictions on the matrix. Let Or be the class of formulas in Kr having disjunctive normal forms with only two disjuncts. Theorem 2 sharpens Orevkov's proof of the unsolvability of Or ([Or]; see also [LeGo]).

Theorem 2. Let D be the class of formulas in Or with just two predicate letters, both pentadic; then D is a reduction class for satisfiability.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 41 , Issue 2 , June 1976 , pp. 341 - 362
Copyright
Copyright © Association for Symbolic Logic 1976

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

Research partially supported by ARPA Grant F19628-71-C-0174. Theorem 1, the main result of this paper, was announced in [Le 1] and appears as Theorem III of [Le 2].

References

REFERENCES

[Aa] 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
[AaLe] Aanderaa, S. O. and Lewis, H. R., Prefix classes of Krom formulas, this Journal, vol. 38 (1973), pp. 628–642.Google Scholar
[Bö] Börger, E., Reduktionstypen in Krom- und Hornformeln, Inauguraldissertation, West-fälische Wilhelms-Universität, Münster, 1971.Google Scholar
[DG] Dreben, B. S. and Goldfarb, W. D., A systematic treatment of the decision problem (in preparation).Google Scholar
[G] Goldfarb, W. D., On decision problems for quantification theory, Ph.D. thesis, Harvard University, 1974.Google Scholar
[KMW] Kahr, A. S., Moore, E. F. and Wang, H., Entscheidungsproblem reduced to the ∀∃∀ case, Proceedings of the National Academy of Sciences of the U.S.A., vol. 48 (1962), pp. 365–377.CrossRefGoogle Scholar
[Kr] 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
[Le 1] Lewis, H. R., Krom formulas with one dyadic letter, Notices of the American Mathematical Society, vol. 20 (1973), p. A-500.Google Scholar
[Le 2] Lewis, H. R., Herbrand expansions and reductions of the decision problem, Ph.D. thesis, Harvard University, 1974.Google Scholar
[LeGo] 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
[Or] Orevkov, V. P., Two undecidable classes of formulas in classical predicate calculus, Seminars in Mathematics, V. A. Steklov Mathematical Institute, Leningrad, vol. 8 (1974), pp. 98–102; Consultants Bureau, New York, 1969.Google Scholar
[Po] Post, E., A variant of a recursively unsolvable problem, Bulletin of the American Mathematical Society, vol. 52 (1946), pp. 264–268.CrossRefGoogle Scholar
[Re] Reynolds, J. C., Transformational systems and the algebraic structure of atomic formulas, Machine intelligence 5 (Meltzer, B. and Michie, D., Editors), American Elsevier Publishing Company, New York, 1970, pp. 135–152.Google Scholar
[Sc] Scanlon, T. M., The consistency of number theory via Herbrand's theorem, this Journal, vol. 38 (1973), pp. 29–58.Google Scholar
[Sh] Shannon, C. E., A universal Turing machine with two internal states, Automata Studies (Shannon, C. E. and McCarthy, J., Editors), Princeton University Press, Princeton, New Jersey, 1956, pp. 157–165.Google Scholar