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
PB - Springer-Verlag GmbH
ER -