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