Abstract
A proof procedure based on a theorem of Herbrand and utilizing the matching technique of Prawitz is presented. In general, Herbrand-type proof procedures proceed by generating ever increasing numbers of candidates for the truth-functionally contradictory statement the procedures seek. A trial is successful when some candidate is in fact a contradictory statement. In procedures to date the number of candidates developed before a contradictory statement is found (if one is found) varies roughly exponentially with the size of the contradictory statement. (“Size” might be measured by the number of clauses in the conjunctive normal form of the contradictory statement.) Although basically subject to the same rate of growth, the procedure introduced here attempts to drastically trim the number of candidates at an intermediate level of development. This is done by retaining beyond a certain level only candidates already “partially contradictory.” The major task usually is finding the partially contradictory sets. However, the number of candidate sets required to find these subsets of the contradictory set is generally much smaller than the number required to find the full contradictory set.
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
References
Chinlund, T., Davis, M., Hinman, P., AND McIlroy, M. D. Theorem-proving by matching. Submitted for publication.
Davis, M. Eliminating the irrelevant from mechanical proofs. Proc. Symp. Appl. Math. XV (1963), 15–30.
Friedman, J. A semi-decision procedure for the functional calculus. J. ACM 10 (1963), 1–24.
Prawitz, D. An improved proof procedure. Theoria 26 (1960), 102–139.
Quine, W. V. A proof procedure for quantification theory. J. Symbolic Logic 20 (1955), 141–149.
Robinson, J. A. A machine-oriented logic based on the resolution principle. J. ACM 12 (1965), 23–41.
Wos, L., Carson, D., AND Robinson, G. The unit preference strategy in theorem proving. Proc. AFIPS 1964 Fall Joint Comput. Conf., Vol. 26, Pt. II, pp. 615–621 ( Spartan Books, Washington, D. C. ).
Wos, L., D.Robinson, G., AND Carson, D. Efficiency and completeness of the set of support strategy in theorem proving. J. ACM 12 (1965), 536–541.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1968 Association for Computing Machinery, Inc.
About this chapter
Cite this chapter
Loveland, D.W. (1968). Mechanical Theorem-Proving by Model Elimination. 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_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-81955-1_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-81957-5
Online ISBN: 978-3-642-81955-1
eBook Packages: Springer Book Archive