#### 4.4 Automatic theorem proving

MacLogic's theorem prover for classical logic is based on the
sequent calculus LK of Gentzen. Like the rest of MacLogic, it
is implemented in Prolog. The monograph
by Melvin Fitting (see Bibliography)
is an excellent coverage of this kind of approach. Difficulties
arise with quantifiers, and we adopt the tricks involving Skolem
functions and unification outlined by Fitting to reduce these
difficulties. Nevertheless, MacLogic's theorem prover is not complete:
but we believe that whatever answer it gives can be relied on,
i.e. it can recognise when it has given an answer which may be
wrong, and tells you so. Changing the level parameter may or may
not give you a more informative answer.

Fitting's book actually outlines
the methods of so-called "semantic tableaux": we regard
these as a notational variant of the sequent calculus, with a
trivial translation betwen the two.

For intuitionistic and minimal logic, roughly the same approach
is adopted, using Gentzen's calculus LJ (or LM for minimal logic).
In fact, a variant described elsewhere (see the paper
by Dyckhoff mentioned in the Bibliography)
is used instead, to avoid some problems with non-termination arising
with the use of LJ.

The file "ATP Help" gives some more detail of how
the automatic theorem prover can be controlled: access it on-line
via the ATP item in the Help
menu.