Experiments with an Automatic Theorem-Prover HavingPartial 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 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. CACM November, 1973 Slagle, J. R. Norton, L. M. theorem-proving, partial ordering, resolution, hyper-resolution, P1-resolution, paramodulation, inference rules, heuristics 3.64 3.66 CA731106 JB January 20, 1978 10:10 AM 2356 4 2420 2420 4 2420 2874 4 2420 3143 4 2420 2227 5 2420 2420 5 2420 2420 5 2420 2420 5 2420