Proving Harder Theorems by Axiom Reduction

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.

• Type: Conference
• Year: 2003
• Where: FLAIRS
• Authors: Geoff Sutcliffe, Alexander Dvorský
• Keywords: Artificial Intelligence, Atp System, Automated Theorem Proving, FLAIRS 2003, Unnecessary Axioms