A Summary of Inference Rules Used by Argonne's Automated Deduction Software

The diverse inference rules were formulated with the objective of providing various types of reasoning capability. In various combinations, the inference rules have been used by In all of our successes, one or more inference rules played a key role. Experiments show that, for attacking deep and unrelated questions, a variety of inference rules is needed. Among the differences, some rules focus on but two hypotheses, and some on two or more; some focus on building in equality; some focus on drawing conclusions free of logical or, and some free of logical not. Every inference rule is required to be sound, yielding conclusions that follow logically and inevitably from the hypotheses in use.

See Automated Reasoning: Introduction and Applications for more complete definitions of many of these inference rules.


Contents

  1. Binary Resolution
  2. Factoring
  3. Hyperresolution
  4. UR-resolution
  5. Unit Deletion
  6. Paramodulation
  7. Negative Paramodulation
  8. Linked Inference Rules
  9. Geometric Rule

Binary Resolution

Binary resolution always focuses on two clauses and one literal in each. To admit a conclusion, the literals must be opposite in sign and alike in predicate, and there must exist a unifier (substitution of terms for variables) to otherwise make them identical. If a conclusion results, it is obtained by applying the unifier to the two clauses excluding the two literals in focus, and taking the union of the transformed literals.

Factoring

Factoring always focuses on one clause at a time and on two literals in that clause. An application of factoring yields a conclusion if and only if the two literals in focus are alike in sign and if there exists a unifier (substitution of terms for variables) whose use makes the two literals identical. The conclusion is obtained by applying the unifier to the clause and merging the identical literals.

In Otter, factoring is implemented in two ways: as an inference rule as described in the preceding paragraph, and as a simplification rule, which applies when the conclusion is logically equivalent to the original clause.


Hyperresolution

Hyperresolution focuses on two or more clauses, requiring that one of the clauses (the nucleus) contain at least one negative literal and the remaining (the satellites) contain no negative literals. Briefly, a conclusion is yielded if a unifier (substitution of terms for variables can be found that, when applied, makes identical (except for sign) pairs of literals, one negative literal from the nucleus with one positive from a satellite. The conclusion is yielded by, ignoring the paired literals, applying the unifier simultaneously to the nucleus and the satellites and taking the union of the resulting literals.

Otter's implementation of hyperresolution has two extra features. First, it can be restricted so that only ``largest'' literals in satellites can be resolved; this restriction can reduce redundancy for non-Horn clauses. Second, the negative literals in the nuclei can be evaluable instead of resolvable; This allows some amount of "programming" of Otter using built-in operations.


UR-resolution

UR-Resolution focuses on two or more clauses, requiring that one of the clauses (the nucleus) contain at least two literals and the remaining (the satellites) contain exactly one literal. Briefly, a conclusion is yielded if a unifier (substitution of terms for variables can be found that, when applied, makes identical (except for being opposite in sign) pairs of literals, one literal from the nucleus with one from a satellite. The conclusion is yielded by, ignoring the paired literals, applying the unifier simultaneously to the nucleus and the satellites and taking the union of the resulting literals.

Unit Deletion

Unit Deletion acts rather like demodulation, automatically removing a literal in a clause when a unit clause exists that unifies with the literal, that is opposite in sign, and such that the unification does not affect the variables in the literal in question.

Paramodulation

Paramodulation always focuses on two clauses, requiring that one of the clauses contain at least one literal asserting the equality of two expressions. For an application of paramodulation to succeed, there must exist a unifier (substitution of terms for variables) that, when used, makes identical one argument of a chosen positive equality literal in one clause and one chosen term in the other clause. If r is the chosen argument, s the other argument of the positive equality literal, t the chosen term, and U the unifier, the conclusion is obtained by applying U to both clauses, then replacing U(t) with U(s), and finally, except for the positive equality literal, taking the union of the transformed remaining literals. (With the exception of reflexivity, x = x, the nature of paramodulation permits the omission of the usual axioms for equality.) Because of the potential fecundity of using paramodulation (from being term-oriented rather than literal-oriented), various restriction strategies are recommended. They include restricting the choice of argument (in the positive equality literal) to just the lefthand argument, to just the righthand argument, and to arguments that are not merely a variable. Also recommended is restricting the chosen term to one that is not merely a variable.

Negative Paramodulation

The inference rule negative paramodulation reasons from negated equalities rather than equalities. The rule is sound if the functions involved satisfy certain cancellation-like properties. For example, from A<>B and AC=D, we can derive BC<>D by negative paramodulation provided that right cancellation holds for product.

L. Wos and W. McCune, ``Negative Paramodulation'', Proceedings of CADE-8, Springer-Verlag Lecture Notes in Computer Science #230, 229-239 (1986).


Linked Inference Rules

Linked inference rules relax the syntactic constraints of ordinary inference rules by allowing link clauses to serve as bridges between clauses that initiate inferences and clauses that complete inferences.

L. Wos, R. Veroff, B. Smith, and W. McCune, ``The Linked Inference Principle, II: The User's Viewpoint'', Proceedings of CADE-7, Springer-Verlag Lecture Notes in Computer Science #170, 316-332 (1984).

R. Veroff and L. Wos, ``The Linked Inference Principle, I: The Formal Treatment'', Journal of Automated Reasoning 8(2), 213-274 (1992).

Linked UR-Resolution

Linked UR-resolution generalizes UR-resolution by allowing nonunit clauses to link the nucleus to satellite clauses (units).

Linked Hyperresolution

Linked Hyperresolution generalizes hyperresolution by allowing clauses (links) to connect literals in the nucleus with literals in the satellites. A link typically relies on one of its positive literals to unify with a negative literal in the nucleus, and on one of its negative literals to unify with a positive literal in a satellite.

Linked Paramodulation

Linked paramodulation generalizes binary paramodulation by allowing equalities to ``transform'' terms before or after ordinary binary paramodulation takes place.

Geometric Rule

R. Padmanabhan's inference rule `=(gL)=>' allows one to prove, within first-order equational logic, theorems about cubic curves in the projective plane. See gL results for examples.

R. Padmanabhan and W. McCune, ``Automated Reasoning about Cubic Curves'', Computers and Mathematics with Applications 29(2), 17-26 (1995).


These activities are projects of the Mathematics and Computer Science Division of Argonne National Laboratory.

Larry Wos / wos@mcs.anl.gov