Proving Harder Theorems by Axiom Reduction

Geoff Sutcliffe and Alexander Dvorsky

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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.