Thumbnail
Access Restriction
Subscribed

Author Fleisig, S. ♦ Loveland, D. ♦ Smiley, A. K. ♦ Yarmush, D. L.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©1974
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
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.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1974-01-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 21
Issue Number 1
Page Count 16
Starting Page 124
Ending Page 139


Open content in new tab

   Open content in new tab
Source: ACM Digital Library