Hostname: page-component-76fb5796d-wq484 Total loading time: 0 Render date: 2024-04-25T16:49:24.278Z Has data issue: false hasContentIssue false
  • English
  • Français

On simplifying the matrix of a wff

Published online by Cambridge University Press:  12 March 2014

Peter Andrews
Peter Andrews*
Affiliation:
Carnegie-Mellon University
Get access Rights & Permissions [Opens in a new window]

Extract

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 … ∀xκ∃y1 … ∃ym∀z1 … ∀zn. 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.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 33 , Issue 2 , 23 July 1968 , pp. 180 - 192
Copyright
Copyright © Association for Symbolic Logic 1968

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

References

[1]Church, Alonzo, A formulation of the simple theory of types, this Journal, vol. 5 (1940), pp. 56–68.Google Scholar
[2]Church, Alonzo, Introduction to mathematical logic, vol. I, Princeton University Press, Princeton, N.J., 1956.Google Scholar
[3]Friedman, Joyce, A semi-decision procedure for the functional calculus, Journal of the Association for Computing Machinery, vol. 10 (1963), pp. 1–24.CrossRefGoogle Scholar
[4]Friedman, Joyce, A computer program for a solvable case of the decision problem, Journal of the Association for Computing Machinery, vol. 10 (1963), pp. 348–356.CrossRefGoogle Scholar
[5]Friedman, Joyce, A new decision procedure in logic with a computer realization, Ph.D. thesis, Harvard University, 1964.Google Scholar
[6]Henkin, Leon, Completeness in the theory of types, this Journal, vol. 15 (1950), pp. 81–91.Google Scholar
[7]Quine, W. V., A proof procedure for quantification theory, this Journal, vol. 20 (1955), pp. 141–149.Google Scholar
[8]Robinson, J. A., A machine-oriented logic based on the resolution principle, Journal of the Association for Computing Machinery, vol. 12 (1965), pp. 23–41.CrossRefGoogle Scholar
[9]Wang, Hao, Logic of many-sorted theories, this Journal, vol. 17 (1952), pp. 105–116.Google Scholar