An Implementation of the Model Elimination Proof Procedure

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

An Implementation of the Model Elimination Proof Procedure

Full text

Pdf (1.09 MB)

Source

Journal of the ACM (JACM) archive
Volume 21 , Issue 1 (January 1974) table of contents

Pages: 124 - 139

Year of Publication: 1974

ISSN:0004-5411

Authors

S. Fleisig	Courant Institute of Mathematical Sciences, New York University, 251 Mercer Street, New York, NY
D. Loveland	Duke University, Durham, NC and Courant Institute of Mathematical Sciences, New York University, 251 Mercer Street, New York, NY
A. K. Smiley, III	Shared Educational Computer Systems, Inc., Poghkeepsie, NY and Courant Institute of Mathematical Sciences, New York University, 251 Mercer Street, New York, NY
D. L. Yarmush	Courant Institute of Mathematical Sciences, New York University, 251 Mercer Street, New York, NY

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 0, Downloads (12 Months): 22, Citation Count: 8

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/321796.321807 What is a DOI?

ABSTRACT

The model elimination (ME) and resolution algorithms for mechanical theorem-proving were implemented so as to maximize shared features. The identical data structures and large amount of common programming permit meaningful comparisons when the two programs are run on standard problems. ME does better on some classes of problems, and resolution better on others. The depth-first search strategy used in this ME implementation affects the performance profoundly. Other novel features in the implementation are new control parameters to govern extensions, and modified rules for generating and rejecting chains. The resolution program incorporates unit preference and set-of-support. An appendix reproduces the steps of a machine-derived ME refutation.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Joyce Friedman, A Semi-Decision Procedure for the Functional Calculus, Journal of the ACM (JACM), v.10 n.1, p.1-24, Jan. 1963 [doi>10.1145/321150.321151]
	2	GLASNER, J., OCKEN, S., ROS~NBERG, D., SCHWARTZ, J., SHAPIRO, G., AND SILVERMAS, A. The Nu-Speak System. NYU Rep., NYO-1480-9 (Nov. 1964), 107 pp.
	3	KOWALSKI, R., AND KUF.HNER, D. Linear resolution with selection function. Artif. lntell. 2 (1971), 227-260.
	4	Donald W. Loveland, Mechanical Theorem-Proving by Model Elimination, Journal of the ACM (JACM), v.15 n.2, p.236-251, April 1968 [doi>10.1145/321450.321456]
	5	D. W. Loveland, A Simplified Format for the Model Elimination Theorem-Proving Procedure, Journal of the ACM (JACM), v.16 n.3, p.349-363, July 1969 [doi>10.1145/321526.321527]
	6	LOVELAND, D.W. Theorem proving combining model elimination and resolution. In Machine Intelligence $, B. Meltzer and D. Michie, Eds., Edinburgh U. Press, Edinburgh, 1969, pp. 73-86.
	7	D. W. Loveland, A Unifying View of Some Linear Herbrand Procedures, Journal of the ACM (JACM), v.19 n.2, p.366-384, April 1972 [doi>10.1145/321694.321706]
	8	LUCKH:.M, D. Some tree-pairing strategies for theorem-proviug. In Machine In~~Zligence ~, E. Dale and D. Meltzer, Eds., Oliver and Boyd, Edinburgh, 1968, pp. 95-112.
	9	J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
	10	Wos, L., CARSON, D. F., AND ROBINSON, G.A. The unit preference strategy in theorem proving. Proc. AFIPS 1964 FJCC, Vol. 26, Spartan Books, New York, pp. 615-621.
	11	Lawrence Wos , George A. Robinson , Daniel F. Carson, Efficiency and Completeness of the Set of Support Strategy in Theorem Proving, Journal of the ACM (JACM), v.12 n.4, p.536-541, Oct. 1965 [doi>10.1145/321296.321302]
	12	Lawrence Wos , George A. Robinson , Daniel F. Carson , Leon Shalla, The Concept of Demodulation in Theorem Proving, Journal of the ACM (JACM), v.14 n.4, p.698-709, Oct. 1967 [doi>10.1145/321420.321429]

CITED BY 8

	Fumiaki Okushi , Allen Van Gelder, Persistent and Quasi-Persistent Lemmas in Propositional Model Elimination, Annals of Mathematics and Artificial Intelligence, v.40 n.3-4, p.373-401, March 2004
	Fumiaki Okushi, Parallel cooperative propositional theorem proving, Annals of Mathematics and Artificial Intelligence, v.26 n.1-4, p.59-85, 1999
	Allen Van Gelder , Fumiaki Okushi, A propositional theorem prover to solve planning and other problems, Annals of Mathematics and Artificial Intelligence, v.26 n.1-4, p.87-112, 1999
	Allen Van Gelder , Fumiaki Okushi, Lemma and cut strategies for propositional model elimination, Annals of Mathematics and Artificial Intelligence, v.26 n.1-4, p.113-132, 1999
	Allen Van Gelder, Autarky Pruning in Propositional Model Elimination Reduces Failure Redundancy, Journal of Automated Reasoning, v.23 n.2, p.137-193, August 1999
	O. L. Astrachan , D. W. Loveland, The Use of Lemmas in the Model Elimination Procedure, Journal of Automated Reasoning, v.19 n.1, p.117-141, August 1997
	Andrea Formisano , Alberto Policriti, T-Resolution: Refinements and Model Elimination, Journal of Automated Reasoning, v.22 n.4, p.433-483, May 1999
	L. Fribourg, A superposition oriented theorem prover, Proceedings of the Eighth international joint conference on Artificial intelligence, p.923-925, August 08-12, 1983, Karlsruhe, West Germany