Lewis M. Norton
Author Archives
Experiment with an automatic theorem-prover having partial ordering inference rules
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.
Shape the Future of Computing
ACM encourages its members to take a direct hand in shaping the future of the association. There are more ways than ever to get involved.
Get Involved