Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

ECAI

2004

Springer

2004

Springer

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...

Added |
20 Aug 2010 |

Updated |
20 Aug 2010 |

Type |
Conference |

Year |
2004 |

Where |
ECAI |

Authors |
Simon Colton, Alison Pease |

Comments (0)