Prover9 FOF Reduction
set(fof_reduction).
Attempts to reduce a problem to a set of independent subproblems.
An Extreme Example
Without FOF reduction:
prover9 -f andrews-0.in > andrews-0.out
With FOF reduction:
prover9 -f andrews.in > andrews.out
Notes
- It works be reducing scopes of quantifiers, normal form conversion, eliminating redundant subformulas.
- It can be explosive, so it gives up after a few seconds.
- It could be made more powerful.
- For propositional problems, it is a (very slow) decision procedure.