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