Abstract
In [3], [4], and [5] Joyce Friedman formulated and investigated certain rules which constitute a semi-decision procedure for wffs of first order predicate calculus in closed prenex normal form with prefixes of the form ∀x1 ...∀xk∃y1 ...∃Ym∀z1 ...∀z n . Given such a wff QM,where Q is the prefix and M is the matrix in conjunctive normal form, Friedman’s rules can be used, in effect, to construct a matrix M* which is obtained from M by deleting certain conjuncts of M. Obviously, ⊢QM⊃QM* Using the Herbrand-Gödel theorem for first order predicate calculus, Friedman showed that ⊢QM if and only if ⊢QM*. Clearly if M* is the empty conjunct (i.e., a tautology), ⊢QM* so ⊢QM. Friedman also showed that for certain classes of wffs, such as those in which m ≤ 2 or n = 0 in the prefix above, ⊢QM if and only if M* is the empty conjunct. Hence for such classes of wffs the rules constitute a decision procedure. Computer implementation [4] of the procedure has shown it to be quite efficient by present standards.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
Bibliography
Alonzo Church,A formulation of the simple theory of types,this Journal, vol. 5 (1940), pp. 56–68.
Alonzo Church, Introduction to mathematical logic, vol. I, Princeton University Press, Princeton, N.J., 1956.
Joyce Friedman, A semi-decision procedure for the functional calculus, Journal of the Association for Computing Machinery, vol. 10 (1963), pp. 1–24.
Joyce Friedman, A computer program for a solvable case of the decision problem, Journal of the Association for Computing Machinery, vol. 10 (1963), pp. 348–356.
Joyce Friedman, A new decision procedure in logic with a computer realization, Ph.D. thesis, Harvard University, 1964.
Leon Henkin, Completeness in the theory of types,this Journal, vol. 15 (1950), pp. 81–91.
W. V. Quine, A proof procedure for quantification theory, this Journal, vol. 20 (1955), pp. 141–149.
J. A. Robinson, A machine-oriented logic based on the resolution principle, Journal of the Association for Computing Machinery, vol. 12 (1965), pp. 23–41.
Hao Wang, Logic of many-sorted theories,this Journal, vol. 17 (1952), pp. 105–116.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1968 Association for Symbolic Logic
About this chapter
Cite this chapter
Andrews, P.B. (1968). On Simplifying the Matrix of a WFF. In: Siekmann, J.H., Wrightson, G. (eds) Automation of Reasoning. Symbolic Computation. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-81955-1_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-81955-1_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-81957-5
Online ISBN: 978-3-642-81955-1
eBook Packages: Springer Book Archive