24
D.W. LOVELAND
where variables can
be
instantiated to fit the application. We have
discussed rewrite rule systems already in the context of equa-
tional theories. Rewrite systems are widely used, both as the
major inference device and as a component system within larger
systems. See Boyer-Moore [BM2] or Winker and Wos [WWl] (also
Wos, this volume) for example systems using rewrite rules.
Algebraic simplification -- usually a special package which
reduces algebraic expressions to a normal form to facilitate
further processing. Such systems are usually implemented using
rewrite rules. Algebraic simplifiers are only an example of
simplification packages, but are the most important example and
one having reached a high degree of sophistication (e.g., see
. [MFl]) ..
Natural inference systems -- predominantly backward chain-
ing inference systems employing many inference rules. Such sys-
tems differ from many traditional logic systems (in particular,
resolution) by not trying to economize on inference rules (the
economy being useful when one wishes to prove theorems
about
logics) and by avoiding symmetric normal forms. Asymmetry is
prized in human simulation systems: A
-+
B and -A v B are logi-
cally equivalent but the former often reveals a use preference
over
-B-+ -A.
In particular, conjunctive (disjunctive) normal
form is avoided. The Bledsoe ATP prover [BTl] is an excellent
example of a natural inference system. The problem reduction
format, mentioned in our discussion of resolution refinements, is a
basic format for structuring proof exploration for natural infer-
ence systems.
Control of search direction -- the ability to chain forward or
backward as is warranted by the local situation. Although back-
ward chaining from the goal towards the premises generally is the
preferable choice of search direction, it is
of~en
wise to generate
Previous Page Next Page