
[full paper] 
Simon Colton, Alison Pease
Automated deduction systems are, in general, not very flexible. In most cases, they assume that the conjecture supplied is true and in all cases, they assume that the conjecture supplied is well formed: the definitions of the concepts related by the conjecture are correct and are the ones the user is really interested in. This does not reflect the more organic processes at work in human mathematics, whereby sketch conjectures are hypothesised and revised in the light of counterexamples, and sketch proofs are slowly improved alongside alterations to the theorem statement until an interesting, proved, result is achieved. Drawing on ideas from Lakatos's philosophy of mathematics, we demonstrate how greater flexibility in automated reasoning can be achieved. In particular, we have implemented a system which is able to take open conjectures and either prove them if true, or modify them to something which is true if the original were false. In the latter case, the system uses the Mace model generator to supply examples supporting the conjecture and examples falsifying it, then the HR machine learning system forms a theory using these examples. Our system extracts concepts which define a subset of the supporting examples and this enables it to perform Lakatosstyle techniques such as counterexamplebarring, strategic withdrawal and piecemeal exclusion. This produces modified hypotheses which are then proved by the Otter theorem prover, and shown to the user. We show the effectiveness of this approach by modifying nontheorems taken from the TPTP library of first order theorems.
Keywords: Theorem Proving, Machine Learning, Model Generation, Automated Mathematics, Philosophy of Mathematics, Concept Formation
Citation: Simon Colton, Alison Pease: Lakatosstyle Automated Theorem Modification. In R.López de Mántaras and L.Saitta (eds.): ECAI2004, Proceedings of the 16th European Conference on Artificial Intelligence, IOS Press, Amsterdam, 2004, pp.975976.