Thumbnail
Access Restriction
Subscribed

Author Slagle, James R. ♦ Norton, Lewis M.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Language English
Subject Keyword Inference rules ♦ Heuristics ♦ Hyper-resolution ♦ Partial ordering ♦ Theorem-proving ♦ Paramodulation ♦ P1-resolution ♦ Resolution
Abstract Automatic theorem-provers need to be made much more efficient. With this in mind, Slagle has shown how the axioms for partial ordering can be replaced by built-in inference rules when using a particular theorem-proving algorithm based upon hyper-resolution and paramodulation. The new rules embody the transitivity of partial orderings and the close relationship between the ⊂ and ⊆ predicates. A program has been developed using a modified version of these rules. This new theorem-prover has been found to be very powerful for solving problems involving partial orderings. This paper presents a detailed description of the program and a comprehensive account of the experiments that have been performed with it.
Description Affiliation: National Institutes of Health, Bethesda, MD (Slagle, James R.; Norton, Lewis M.)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2005-08-01
Publisher Place New York
Journal Communications of the ACM (CACM)
Volume Number 16
Issue Number 11
Page Count 7
Starting Page 682
Ending Page 688


Open content in new tab

   Open content in new tab
Source: ACM Digital Library