Reformation: A Domain-Independent Algorithm for Theory Repair

We describe reformation, a new algorithm for the automated repair of faulty logical theories. A fault is revealed by a reasoning failure: either the proof of a false conjecture or the failure to prove a true conjecture. Repair suggestions are systematically extracted via analysis of (un)successful unifications of formulae in (broken) proofs. These suggestions will either unblock a wanted but unsuccessful unification attempt or block an unwanted but successful unification. In contrast to traditional abduction and belief revision mechanisms, the repairs are to the {\em language} of the theory as well as to the axioms. The intention is that the language repairs suggested by reformation complement these axiom deleting and adding repairs, adding to the overall capability of theory repair and evolution. Reformation is self-inverse in that any blocking repair can be undone by an unblocking one, and vice versa. This self-inverse property provides some assurance that reformation repairs are minimal.