ECAI 2004 Conference Paper

[full paper]

Lakatos-style Automated Theorem Modification

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 Lakatos-style techniques such as counterexample-barring, 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 non-theorems 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: Lakatos-style 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.975-976.