Automated Theorem Proving (ATP) problems may contain unnecessary axioms, either because some of the axiomati-zation 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.
展开▼
