The TM system for repairing non-theorems

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

    Research output: Contribution to journalSpecial issuepeer-review

    9 Citations (Scopus)


    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.
    Original languageEnglish
    Pages (from-to)87-101
    Number of pages15
    JournalElectronic Notes in Theoretical Computer Science
    Issue number3
    Publication statusPublished - 18 Jul 2005
    EventIJCAR 2004 Workshop W1: Workshop on Disproving - Non-Theorems, Non-Validity, Non-Provability - University College Cork, Cork, Ireland
    Duration: 5 Jul 20045 Jul 2004


    Dive into the research topics of 'The TM system for repairing non-theorems'. Together they form a unique fingerprint.

    Cite this