Lakatos-style methods in automated reasoning
Simon Colton, Alison Pease · 2003
We advocate increased flexibility in automated reasoning, whereby a reasoning agent is able to correct the statement of a given faulty conjecture in order to prove that the modified theorem is true. Such alterations are common in mathematics. In particular, in his book `Proofs and Refutations', Imre Lakatos prescribes various techniques for the modification of a faulty conjecture within a social setting (a hypothesised mathematics class). This has inspired a multi-agent approach to automating Lakatos-style techniques, and we give details of the implementation of these methods within (and on top of) the HR automated theory formation system. We report on the progress of this project and supply illustrative results from sessions using the enhanced system.