Discovery - University of Dundee - Online Publications

Library & Learning Centre

The TM system for repairing non-theorems

The TM system for repairing non-theorems

Research output: Contribution to journalSpecial issue

View graph of relations

Authors

  • Simon Colton (Lead / Corresponding author)
  • Alison Pease (Lead / Corresponding author)

Research units

Info

Original languageEnglish
Pages (from-to)87-101
Number of pages15
JournalElectronic Notes in Theoretical Computer Science
Volume125
Issue number3
DOIs
StatePublished - 18 Jul 2005
EventIJCAR 2004 Workshop W1: Workshop on Disproving - Non-Theorems, Non-Validity, Non-Provability - Cork, Ireland

Abstract

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 in the TM system through an interaction of the HR machine learning program, the Otter theorem prover and the Mace model generator. Given a non-theorem, Mace is used to generate examples which support the non-theorem, and examples which falsify it. HR then invents concepts which categorise these examples and TM uses these concepts to modify the original non-theorem into specialised theorems which Otter can prove. The methods employed by TM are inspired by the piecemeal exclusion, strategic withdrawal and counterexample barring methods described in Lakatos's philosophy of mathematics. In addition, TM can also determine which modified theorems are likely to be interesting and which are not. We demonstrate the effectiveness of this approach by modifying non-theorems taken from the TPTP library of first order theorems. We show that, for 98 non-theorems, TM produced meaningful modifications for 81 of them. This work forms part of two larger projects. Firstly, we are working towards a full implementation both of the reasoning and the social interaction notions described by Lakatos. Secondly, we are aiming to show that the combination of reasoning systems such as those used in TM will lead to a new generation of more powerful AI systems.

Documents

DOI

Library & Learning Centre

Contact | Accessibility | Policy