Lakatos-style automated theorem modification

Simon Colton, Alison Pease

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review


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.

Original languageEnglish
Title of host publicationECAI 2004 - 16th European Conference on Artificial Intelligence, including Prestigious Applications of Intelligent Systems, PAIS 2004 - Proceedings
EditorsRamon Lopez de Mantaras, Lorenza Saitta
PublisherIOS Press
Number of pages2
ISBN (Electronic)9781586034528
Publication statusPublished - 1 Jan 2004
Externally publishedYes
EventEuropean Conference on Artificial Intelligence 2004 - Valencia, Spain
Duration: 22 Aug 200427 Aug 2004
Conference number: 16th (Proceedings)

Publication series

NameFrontiers in Artificial Intelligence and Applications
ISSN (Print)0922-6389


ConferenceEuropean Conference on Artificial Intelligence 2004
Abbreviated titleECAI 2004
Internet address

Cite this