Lakatos-style automated theorem modification

Simon Colton; Alison Pease

Lakatos-style automated theorem modification

Simon Colton, Alison Pease

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

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 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 language	English
Title of host publication	ECAI 2004 - 16th European Conference on Artificial Intelligence, including Prestigious Applications of Intelligent Systems, PAIS 2004 - Proceedings
Editors	Ramon Lopez de Mantaras, Lorenza Saitta
Publisher	IOS Press
Pages	975-976
Number of pages	2
ISBN (Electronic)	9781586034528
Publication status	Published - 1 Jan 2004
Externally published	Yes
Event	European Conference on Artificial Intelligence 2004 - Valencia, Spain Duration: 22 Aug 2004 → 27 Aug 2004 Conference number: 16th https://dl.acm.org/doi/proceedings/10.5555/3000001 (Proceedings)

Publication series

Name	Frontiers in Artificial Intelligence and Applications
Volume	110
ISSN (Print)	0922-6389

Conference

Conference	European Conference on Artificial Intelligence 2004
Abbreviated title	ECAI 2004
Country/Territory	Spain
City	Valencia
Period	22/08/04 → 27/08/04
Internet address	https://dl.acm.org/doi/proceedings/10.5555/3000001 (Proceedings)

Cite this

@inproceedings{c5109b12b0c342a5ab0ed5ad876eacfe,

title = "Lakatos-style automated theorem modification",

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

author = "Simon Colton and Alison Pease",

year = "2004",

month = jan,

day = "1",

language = "English",

series = "Frontiers in Artificial Intelligence and Applications",

publisher = "IOS Press",

pages = "975--976",

editor = "\{de Mantaras\}, \{Ramon Lopez\} and Lorenza Saitta",

booktitle = "ECAI 2004 - 16th European Conference on Artificial Intelligence, including Prestigious Applications of Intelligent Systems, PAIS 2004 - Proceedings",

address = "Netherlands",

note = "European Conference on Artificial Intelligence 2004, ECAI 2004 ; Conference date: 22-08-2004 Through 27-08-2004",

url = "https://dl.acm.org/doi/proceedings/10.5555/3000001",

}

Colton, S & Pease, A 2004, Lakatos-style automated theorem modification. in RL de Mantaras & L Saitta (eds), ECAI 2004 - 16th European Conference on Artificial Intelligence, including Prestigious Applications of Intelligent Systems, PAIS 2004 - Proceedings. Frontiers in Artificial Intelligence and Applications, vol. 110, IOS Press, pp. 975-976, European Conference on Artificial Intelligence 2004, Valencia, Spain, 22/08/04.

Lakatos-style automated theorem modification. / Colton, Simon; Pease, Alison.
ECAI 2004 - 16th European Conference on Artificial Intelligence, including Prestigious Applications of Intelligent Systems, PAIS 2004 - Proceedings. ed. / Ramon Lopez de Mantaras; Lorenza Saitta. IOS Press, 2004. p. 975-976 (Frontiers in Artificial Intelligence and Applications; Vol. 110).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

TY - GEN

T1 - Lakatos-style automated theorem modification

AU - Colton, Simon

AU - Pease, Alison

N1 - Conference code: 16th

PY - 2004/1/1

Y1 - 2004/1/1

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

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

UR - http://www.scopus.com/inward/record.url?scp=85017354214&partnerID=8YFLogxK

M3 - Conference Paper

AN - SCOPUS:85017354214

T3 - Frontiers in Artificial Intelligence and Applications

SP - 975

EP - 976

BT - ECAI 2004 - 16th European Conference on Artificial Intelligence, including Prestigious Applications of Intelligent Systems, PAIS 2004 - Proceedings

A2 - de Mantaras, Ramon Lopez

A2 - Saitta, Lorenza

PB - IOS Press

T2 - European Conference on Artificial Intelligence 2004

Y2 - 22 August 2004 through 27 August 2004

ER -

Lakatos-style automated theorem modification

Abstract

Publication series

Conference

Other files and links

Cite this