Advertisement

Author Archives

Research and Advances

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