Sciweavers

ECAI
2004
Springer

Lakatos-Style Automated Theorem Modification

14 years 1 months ago
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...
Simon Colton, Alison Pease
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Where ECAI
Authors Simon Colton, Alison Pease
Comments (0)