Lakatos-Style Automated Theorem Modification

We describe a flexible approach to automated reasoning, where non-theorems can be automatically altered to produce proved results which are related to the original. This is achieved through an interaction of the HR machine learning system, the Otter theorem prover and the Mace model generator, and uses methods inspired by Lakatos's philosophy of mathematics. We demonstrate the effectiveness of this approach by modifying non-theorems taken from the TPTP library of first order theorems. 1 Background Current automated deduction systems are only capable of three types of output when given a conjecture: proof that it is true, proof that it is false, or that the conjecture is still open. We believe that greater flexibility and ability to better handle ill-specified problems would improve reasoning systems. We have implemented a theorem modifier system, TM, which is able to take in a conjecture, try to prove it and if unsuccessful (either because the conjecture is too hard to prove or be...

• Type: Conference
• Year: 2004
• Where: ECAI
• Authors: Simon Colton, Alison Pease
• Keywords: Artificial Intelligence, Conjectures, ECAI 2004, Lakatos's Philosophy, Otter Theorem Prover