Lakatos-style automated theorem modification
Simon Colton, Alison Pease · Discovery Research Portal (University of Dundee) · 2004
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.