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
- The NIUTP/AURA series of the 1970s and early 1980s
- LMA/ITP of the 1980s
- Otter, our current prover
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
- Binary Resolution
- Factoring
- Hyperresolution
- UR-resolution
- Unit Deletion
- Paramodulation
- Negative Paramodulation
- Linked Inference Rules
- Geometric Rule
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 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 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 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 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 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.
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 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 generalizes UR-resolution by allowing nonunit
clauses to link the nucleus to satellite clauses (units).
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 generalizes binary paramodulation by allowing
equalities to ``transform'' terms before or after ordinary binary
paramodulation takes place.
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