Hostname: page-component-7b7567c8c-fvjsw Total loading time: 0 Render date: 2026-11-14T12:30:46.638Z Has data issue: false hasContentIssue false
  • English
  • Français

A reduction class containing formulas with one monadic predicate and one binary function symbol

Published online by Cambridge University Press:  12 March 2014

Charles E. Hughes
Charles E. Hughes*
Affiliation:
University of Tennessee, Knoxville, Tennessee 37916
Get accessRights & Permissions [Opens in a new window]

Abstract

A new reduction class is presented for the satisfiability problem for well-formed formulas of the first-order predicate calculus. The members of this class are closed prenex formulas of the form ∀x∀yC. The matrix C is in conjunctive normal form and has no disjuncts with more than three literals, in fact all but one conjunct is unary. Furthermore C contains but one predicate symbol, that being unary, and one function symbol which symbol is binary.

Information

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 41 , Issue 1 , March 1976, pp. 45 - 49
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.)

Article purchase

Temporarily unavailable

References

REFERENCES

[1] Börger, E., Reduction classes of Krom formulae with only one predicate symbol and function symbols, Notices of the American Mathematical Society, vol. 20 (1973), A–286. Abstract.Google Scholar
[2] Church, A., Introduction to mathematical logic, Vol. I, Princeton University Press, Princeton, N.J., 1956.Google Scholar
[3] Davis, M., Computability and unsolvability, McGraw-Hill, New York, 1958.Google Scholar
[4] Hughes, C. E., Two variable implicational calculi of prescribed many-one degrees of unsolvability, this Journal, vol. 41 (1976), pp. 39–45.Google Scholar
[5] Krom, M. R., The decision problem for formulas in prenex conjunctive normal form with binary disjunction, this Journal, vol. 35 (1970), pp. 210–216.Google Scholar