A Combinator Language for Theorem Discovery

Phil Scott; Jacques Fleuriot

doi:10.1007/978-3-642-31374-5_25

A Combinator Language for Theorem Discovery

Phil Scott, Jacques Fleuriot

School of Informatics

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

We define and implement a combinator language for intermediate lemma discovery. We start by generalising an algebraic data-structure for unbounded search and then extend it to support case-analysis. With our language defined, we expect users to be able to write discoverers which collaborate intelligently in specific problem domains. For now, the language integrates rewriting, forward-deduction, and case-analysis and discovers lemmas concurrently based on an interactive proof context. We argue that the language is most suitable for adding domain-specific automation to mechanically formalised proofs written in a forward-style, and we show how the language is used via a case-study in geometry.

Original language	English
Title of host publication	Intelligent Computer Mathematics
Subtitle of host publication	11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings
Editors	Johan Jeuring, John Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel, Volker Sorge
Publisher	Springer
Pages	371-385
Number of pages	15
ISBN (Electronic)	978-3-642-31374-5
ISBN (Print)	978-3-642-31373-8
DOIs	https://doi.org/10.1007/978-3-642-31374-5_25
Publication status	Published - 2012

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin / Heidelberg
Volume	7362
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/978-3-642-31374-5_25

http://link.springer.com/chapter/10.1007%2F978-3-642-31374-5_25

Cite this

Scott, P., & Fleuriot, J. (2012). A Combinator Language for Theorem Discovery. In J. Jeuring, J. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, & V. Sorge (Eds.), Intelligent Computer Mathematics: 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings (pp. 371-385). (Lecture Notes in Computer Science; Vol. 7362). Springer. https://doi.org/10.1007/978-3-642-31374-5_25

Scott, Phil ; Fleuriot, Jacques. / A Combinator Language for Theorem Discovery. Intelligent Computer Mathematics: 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings. editor / Johan Jeuring ; John Campbell ; Jacques Carette ; Gabriel Dos Reis ; Petr Sojka ; Makarius Wenzel ; Volker Sorge. Springer, 2012. pp. 371-385 (Lecture Notes in Computer Science).

@inproceedings{10c10cecac7446b8a1f72e97a7b54ca3,

title = "A Combinator Language for Theorem Discovery",

abstract = "We define and implement a combinator language for intermediate lemma discovery. We start by generalising an algebraic data-structure for unbounded search and then extend it to support case-analysis. With our language defined, we expect users to be able to write discoverers which collaborate intelligently in specific problem domains. For now, the language integrates rewriting, forward-deduction, and case-analysis and discovers lemmas concurrently based on an interactive proof context. We argue that the language is most suitable for adding domain-specific automation to mechanically formalised proofs written in a forward-style, and we show how the language is used via a case-study in geometry.",

author = "Phil Scott and Jacques Fleuriot",

year = "2012",

doi = "10.1007/978-3-642-31374-5\_25",

language = "English",

isbn = "978-3-642-31373-8",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "371--385",

editor = "Johan Jeuring and John Campbell and Jacques Carette and \{Dos Reis\}, Gabriel and Petr Sojka and Makarius Wenzel and Volker Sorge",

booktitle = "Intelligent Computer Mathematics",

address = "United Kingdom",

}

Scott, P & Fleuriot, J 2012, A Combinator Language for Theorem Discovery. in J Jeuring, J Campbell, J Carette, G Dos Reis, P Sojka, M Wenzel & V Sorge (eds), Intelligent Computer Mathematics: 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings. Lecture Notes in Computer Science, vol. 7362, Springer, pp. 371-385. https://doi.org/10.1007/978-3-642-31374-5_25

A Combinator Language for Theorem Discovery. / Scott, Phil; Fleuriot, Jacques.
Intelligent Computer Mathematics: 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings. ed. / Johan Jeuring; John Campbell; Jacques Carette; Gabriel Dos Reis; Petr Sojka; Makarius Wenzel; Volker Sorge. Springer, 2012. p. 371-385 (Lecture Notes in Computer Science; Vol. 7362).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - A Combinator Language for Theorem Discovery

AU - Scott, Phil

AU - Fleuriot, Jacques

PY - 2012

Y1 - 2012

N2 - We define and implement a combinator language for intermediate lemma discovery. We start by generalising an algebraic data-structure for unbounded search and then extend it to support case-analysis. With our language defined, we expect users to be able to write discoverers which collaborate intelligently in specific problem domains. For now, the language integrates rewriting, forward-deduction, and case-analysis and discovers lemmas concurrently based on an interactive proof context. We argue that the language is most suitable for adding domain-specific automation to mechanically formalised proofs written in a forward-style, and we show how the language is used via a case-study in geometry.

AB - We define and implement a combinator language for intermediate lemma discovery. We start by generalising an algebraic data-structure for unbounded search and then extend it to support case-analysis. With our language defined, we expect users to be able to write discoverers which collaborate intelligently in specific problem domains. For now, the language integrates rewriting, forward-deduction, and case-analysis and discovers lemmas concurrently based on an interactive proof context. We argue that the language is most suitable for adding domain-specific automation to mechanically formalised proofs written in a forward-style, and we show how the language is used via a case-study in geometry.

U2 - 10.1007/978-3-642-31374-5_25

DO - 10.1007/978-3-642-31374-5_25

M3 - Conference contribution

SN - 978-3-642-31373-8

T3 - Lecture Notes in Computer Science

SP - 371

EP - 385

BT - Intelligent Computer Mathematics

A2 - Jeuring, Johan

A2 - Campbell, John

A2 - Carette, Jacques

A2 - Dos Reis, Gabriel

A2 - Sojka, Petr

A2 - Wenzel, Makarius

A2 - Sorge, Volker

PB - Springer

ER -

Scott P, Fleuriot J. A Combinator Language for Theorem Discovery. In Jeuring J, Campbell J, Carette J, Dos Reis G, Sojka P, Wenzel M, Sorge V, editors, Intelligent Computer Mathematics: 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings. Springer. 2012. p. 371-385. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-31374-5_25

A Combinator Language for Theorem Discovery

Abstract

Publication series

Access to Document

Fingerprint

Cite this