Proving Harder Theorems by Axiom Reduction

May 2003

Proceedings of the Sixteenth International Florida Artificial Intelligence Research Society Conference (FLAIRS 2003)

Volume

Proceedings of the Sixteenth International Florida Artificial Intelligence Research Society Conference (FLAIRS 2003)

All Papers

Automated Theorem Proving (ATP) problems may contain unnecessary axioms, either because some of the axiomatization of the theory is irrelevant to the particular theorem, or because the axiomatization is redundant by design. ATP systems do not have effective techniques for detecting that axioms are unnecessary (or unlikely to be necessary) to the proof of a theorem. Axiom reduction removes combinations of axioms from an ATP problem, and submits the resultant axiom-reduced problems to an object ATP system. When a combination of only unnecessary axioms is removed, the problem may be quickly solved.