Scheme-Based Synthesis of Inductive Theories

O. Montano-Rivas; R. McCasland; L. Dixon; Alan Bundy

doi:10.1007/978-3-642-16761-4_31

Scheme-Based Synthesis of Inductive Theories

O. Montano-Rivas, R. McCasland, L. Dixon, Alan Bundy

School of Informatics

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

Abstract / Description of output

We describe an approach to automatically invent/explore new mathematical theories, with the goal of producing results comparable to those produced by humans, as represented, for example, in the libraries of the Isabelle proof assistant. Our approach is based on 'schemes', which are terms in higher-order logic. We show that it is possible to automate the instantiation process of schemes to generate conjectures and definitions. We also show how the new definitions and the lemmata discovered during the exploration of the theory can be used not only to help with the proof obligations during the exploration, but also to reduce redundancies inherent in most theory formation systems. We implemented our ideas in an automated tool, called IsaScheme, which employs Knuth-Bendix completion and recent automatic inductive proof tools. We have evaluated our system in a theory of natural numbers and a theory of lists.

Original language	English
Title of host publication	Advances in Artificial Intelligence
Subtitle of host publication	9th Mexican International Conference on Artificial Intelligence, MICAI 2010, Pachuca, Mexico, November 8-13, 2010, Proceedings, Part I
Editors	Grigori Sidorov, Arturo Hernández Aguirre, Carlos Alberto Reyes García
Publisher	Springer-Verlag GmbH
Pages	348-361
Number of pages	14
ISBN (Print)	978-3-642-16760-7
DOIs	https://doi.org/10.1007/978-3-642-16761-4_31
Publication status	Published - 2010

Publication series

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

Keywords / Materials (for Non-textual outputs)

Mathematical theory exploration
schemes
theorem proving
termination
term rewriting

Access to Document

10.1007/978-3-642-16761-4_31

Full textAccepted author manuscript, 285 KB

http://www.springerlink.com/content/m885557421m7418m/

Cite this

Montano-Rivas, O., McCasland, R., Dixon, L., & Bundy, A. (2010). Scheme-Based Synthesis of Inductive Theories. In G. Sidorov, A. H. Aguirre, & C. A. R. García (Eds.), Advances in Artificial Intelligence: 9th Mexican International Conference on Artificial Intelligence, MICAI 2010, Pachuca, Mexico, November 8-13, 2010, Proceedings, Part I (pp. 348-361). (Lecture Notes in Computer Science; Vol. 6437). Springer-Verlag GmbH. https://doi.org/10.1007/978-3-642-16761-4_31

Montano-Rivas, O. ; McCasland, R. ; Dixon, L. et al. / Scheme-Based Synthesis of Inductive Theories. Advances in Artificial Intelligence: 9th Mexican International Conference on Artificial Intelligence, MICAI 2010, Pachuca, Mexico, November 8-13, 2010, Proceedings, Part I. editor / Grigori Sidorov ; Arturo Hernández Aguirre ; Carlos Alberto Reyes García. Springer-Verlag GmbH, 2010. pp. 348-361 (Lecture Notes in Computer Science).

@inproceedings{500a434a12f847ae8e64109c06f28fa6,

title = "Scheme-Based Synthesis of Inductive Theories",

abstract = "We describe an approach to automatically invent/explore new mathematical theories, with the goal of producing results comparable to those produced by humans, as represented, for example, in the libraries of the Isabelle proof assistant. Our approach is based on 'schemes', which are terms in higher-order logic. We show that it is possible to automate the instantiation process of schemes to generate conjectures and definitions. We also show how the new definitions and the lemmata discovered during the exploration of the theory can be used not only to help with the proof obligations during the exploration, but also to reduce redundancies inherent in most theory formation systems. We implemented our ideas in an automated tool, called IsaScheme, which employs Knuth-Bendix completion and recent automatic inductive proof tools. We have evaluated our system in a theory of natural numbers and a theory of lists.",

keywords = "Mathematical theory exploration, schemes, theorem proving, termination, term rewriting",

author = "O. Montano-Rivas and R. McCasland and L. Dixon and Alan Bundy",

year = "2010",

doi = "10.1007/978-3-642-16761-4_31",

language = "English",

isbn = "978-3-642-16760-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer-Verlag GmbH",

pages = "348--361",

editor = "Grigori Sidorov and Aguirre, {Arturo Hern{\'a}ndez} and Garc{\'i}a, {Carlos Alberto Reyes}",

booktitle = "Advances in Artificial Intelligence",

}

Montano-Rivas, O, McCasland, R, Dixon, L & Bundy, A 2010, Scheme-Based Synthesis of Inductive Theories. in G Sidorov, AH Aguirre & CAR García (eds), Advances in Artificial Intelligence: 9th Mexican International Conference on Artificial Intelligence, MICAI 2010, Pachuca, Mexico, November 8-13, 2010, Proceedings, Part I. Lecture Notes in Computer Science, vol. 6437, Springer-Verlag GmbH, pp. 348-361. https://doi.org/10.1007/978-3-642-16761-4_31

Scheme-Based Synthesis of Inductive Theories. / Montano-Rivas, O.; McCasland, R.; Dixon, L. et al.
Advances in Artificial Intelligence: 9th Mexican International Conference on Artificial Intelligence, MICAI 2010, Pachuca, Mexico, November 8-13, 2010, Proceedings, Part I. ed. / Grigori Sidorov; Arturo Hernández Aguirre; Carlos Alberto Reyes García. Springer-Verlag GmbH, 2010. p. 348-361 (Lecture Notes in Computer Science; Vol. 6437).

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

TY - GEN

T1 - Scheme-Based Synthesis of Inductive Theories

AU - Montano-Rivas, O.

AU - McCasland, R.

AU - Dixon, L.

AU - Bundy, Alan

PY - 2010

Y1 - 2010

N2 - We describe an approach to automatically invent/explore new mathematical theories, with the goal of producing results comparable to those produced by humans, as represented, for example, in the libraries of the Isabelle proof assistant. Our approach is based on 'schemes', which are terms in higher-order logic. We show that it is possible to automate the instantiation process of schemes to generate conjectures and definitions. We also show how the new definitions and the lemmata discovered during the exploration of the theory can be used not only to help with the proof obligations during the exploration, but also to reduce redundancies inherent in most theory formation systems. We implemented our ideas in an automated tool, called IsaScheme, which employs Knuth-Bendix completion and recent automatic inductive proof tools. We have evaluated our system in a theory of natural numbers and a theory of lists.

AB - We describe an approach to automatically invent/explore new mathematical theories, with the goal of producing results comparable to those produced by humans, as represented, for example, in the libraries of the Isabelle proof assistant. Our approach is based on 'schemes', which are terms in higher-order logic. We show that it is possible to automate the instantiation process of schemes to generate conjectures and definitions. We also show how the new definitions and the lemmata discovered during the exploration of the theory can be used not only to help with the proof obligations during the exploration, but also to reduce redundancies inherent in most theory formation systems. We implemented our ideas in an automated tool, called IsaScheme, which employs Knuth-Bendix completion and recent automatic inductive proof tools. We have evaluated our system in a theory of natural numbers and a theory of lists.

KW - Mathematical theory exploration

KW - schemes

KW - theorem proving

KW - termination

KW - term rewriting

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

U2 - 10.1007/978-3-642-16761-4_31

DO - 10.1007/978-3-642-16761-4_31

M3 - Conference contribution

SN - 978-3-642-16760-7

T3 - Lecture Notes in Computer Science

SP - 348

EP - 361

BT - Advances in Artificial Intelligence

A2 - Sidorov, Grigori

A2 - Aguirre, Arturo Hernández

A2 - García, Carlos Alberto Reyes

PB - Springer-Verlag GmbH

ER -

Montano-Rivas O, McCasland R, Dixon L, Bundy A. Scheme-Based Synthesis of Inductive Theories. In Sidorov G, Aguirre AH, García CAR, editors, Advances in Artificial Intelligence: 9th Mexican International Conference on Artificial Intelligence, MICAI 2010, Pachuca, Mexico, November 8-13, 2010, Proceedings, Part I. Springer-Verlag GmbH. 2010. p. 348-361. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-16761-4_31

Scheme-Based Synthesis of Inductive Theories

Abstract / Description of output

Publication series

Keywords / Materials (for Non-textual outputs)

Access to Document

Other files and links

Fingerprint

Automated Theorem Discovery

Cite this

Scheme-Based Synthesis of Inductive Theories

Abstract / Description of output

Publication series

Keywords / Materials (for Non-textual outputs)

Access to Document

Other files and links

Fingerprint

Projects

Automated Theorem Discovery

Cite this