ATP | Menus | Rules | Syntax | Tactics

MacLogic includes an Automatic Theorem Prover (called the "prover" or the "validity-checker"). This is intended mainly to warn of attempts to solve unsolvable problems; it can also be used on its own, via the "Automatic" item of the "Problem" menu. But, first-order logics are generally undecidable: so the prover may give a misleading answer.

The prover is believed to be correct and complete for the non-modal ZERO-ORDER logics: if your problems contain no quantifiers, modal operators, or equations, then the prover's responses can (I believe) be relied on. (Errors to my attention, fast, please! Of course, there are zero-order problems which cannot be solved within reasonable limits of memory and time, whose attempted solution you will have to interrupt.)

If your problem contains one or more quantifiers, then the prover may respond that a problem "may be unsolvable" when it is in fact solvable. (More precisely, it may say the problem is unsolvable at a certain "level".)

The difficulty arises with the rules for universal quantifier elimination and (in classical logic) for existential quantifier introduction: to complete a proof, it may be necessary to use, for example, the former rule several times on a particular quantified formula. One cannot predict in advance how many times this will be necessary. Thus, either one allows an unlimited number of uses, and then the prover will fail to terminate on some hard problems; or one limits the number of uses made of these two rules.

This number can be adjusted from 0 (no use at all) to 7 (seven uses of the rule on EACH formula on EACH branch of the proof tree, which is fairly liberal).

- Level 1 is the default, suitable for almost all elementary problems.
- Some simple-looking problems can only be shown to be solvable by using level 2.
- Higher levels just slow down the rate at which problems are tackled, but are necessary to show that some very hard problems are solvable. Levels less than 4 are adequate for almost anything met at the elementary level.

Adjustment is made either from the "Set validity checker" item in the "Options" menu, or in a dialog ensuing from the "Valid" item in the "Help" menu.

The prover should never say that an unsolvable problem is solvable. (Again, errors to me, fast!)

The prover completely ignores the rules for EQUALITY and MODALITY.

You can INTERRUPT the action of the prover (e.g. if it gets stuck) by typing Command Period. You can tell when the prover is active: the cursor changes, temporarily, to a rotating ball.

ATP | Menus | Rules | Syntax | Tactics