FOF-Prover9

FOF (First-Order Formula) reduction is a method of attempting to simplify a problem by reducing it to an equivalent set of independent subproblems. A trivial example is to reduce the conjecture A <-> B to the pair of problems A -> B and B -> A.

The problem reduction uses a miniscope method [Champeaux-miniscope] that is quite powerful in some cases, but it can easily blow up on complex formulas. Therefore, if the reduction procedure fails to terminate within a few seconds, or if the subproblems it produces are more complex than the original problem, the reduction attempt is aborted (and the user may wish to try the ordinary Prover9 program instead). If the reduction succeeds, each subproblem is given to the ordinary Prover9 search module.

Input files accepted by FOF-Prover9 are the same as those accepted by Prover9, and when FOF-Prover9 runs the search module on a subproblem, is uses all of the options given in the input file.

An Example of FOF Reduction

This example was given by Peter Andrews as a challenge problem for resolution systems in the 1970s. FOF-Prover9's miniscope procedure reduces it to 32 trivial subproblems. (More powerful miniscope methods can solve the problem by reducing it to 0 subproblems.)

fof-prover9 -f andrews.in > andrews.out

Here is the same input run with ordinary Prover9.

prover9 -f andrews.in > andrews.out2

The preceding example is artificial and seems tailor-made for FOF reduction. Other, more realistic examples can be found in the standard set of Prover9 examples.

Next Section: More Programs