Projects per year
Abstract / Description of output
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 selfinverse in that any blocking repair can be undone by an unblocking one, and vice versa. This selfinverse property provides some assurance that reformation repairs are minimal.
Original language  English 

Pages  124 
Number of pages  24 
Publication status  Published  1 Feb 2016 
Fingerprint
Dive into the research topics of 'Reformation: A DomainIndependent Algorithm for Theory Repair'. Together they form a unique fingerprint.Projects
 1 Finished

The integration and interaction of multiple mathematical Reasoning Processes
Bundy, A., Aspinall, D., Colton, S., Fleuriot, J., Gow, J., Grov, G., Ireland, A., Jackson, P., Mcneill, F., Michaelson, G. & Smaill, A.
1/11/15 → 31/10/19
Project: Research