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.