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
Previous Page Next Page