22 D.W. LOVELAND

An ambitious theorem prover now being developed at

Karlsruhe, West Germany, the Markgraf Karl Refutation Procedure

[BEl], promises to be a very significant prover if tt approaches the

capabilities planned for it by its designers. Early reports of prob-

lems run suggest that it compares favorably with other existing

provers. It appears to split our classification, with a heuristic

Supervisor (an overdirector) coupled to a logic engine built

aro~nd

a connection graph prover. Domain specific knowledge is

available via a data bank; in the first version the chosen domain is

automata theory.

The last decade also has seen the invention or amplification of

new techniques for theorem proving. Included here is the connec-

tion graph method as an offshoot of resolution methods (this is

mentioned in the preceding paragraphs). Two techniques not

linked directly to resolution are re:write rule systems, already dis-

cussed, and decision procedures. We comment on the latter

briefly now. The rewrite rule systems and decision procedures

have been featured in applications of theorem provers in non-

mathematical roles, as discussed at the end of the paper.

By a decision procedure we mean a procedure that determines

validity (or satisfiability) of a formula in a theory and halts on any

formula in the theory. The Presburger decision procedure has

already been mentioned. The decision procedures of recent note

have tended to be tests for satisfiability and apply to quantifier-

free first-order theories. Examples are Presburger arithmetic with

uninterpreted function symbols (Shostak [Sh2]), augmented by

array

store

and

select

(Suzuki and Jefferson (SJ

1]);

a set theory

using u ,n, -,

=

,e (Ferro, Omodeo, Schwartz [FOl]) and the theory

of equality with uninterpreted function symbols (Ackerman [Acl],

Nelson and Oppen [NOl], Downey, Sethi and Tarjan [DSl], and oth-

ers).

An

important paper in this regard is that of Nelson and