TY - JOUR
T1 - Scheme-based theorem discovery and concept invention
AU - Montano-Rivas,Omar
AU - McCasland,Roy
AU - Dixon,Lucas
AU - Bundy,Alan
PY - 2012
Y1 - 2012
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 formulae 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 a 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 exploit associative-commutative (AC) operators using ordered rewriting to avoid AC variations of the same instantiation. 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 formulae 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 a 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 exploit associative-commutative (AC) operators using ordered rewriting to avoid AC variations of the same instantiation. 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.
U2 - 10.1016/j.eswa.2011.06.055
DO - 10.1016/j.eswa.2011.06.055
M3 - Article
VL - 39
SP - 1637
EP - 1646
JO - Expert Systems with Applications
T2 - Expert Systems with Applications
JF - Expert Systems with Applications
SN - 0957-4174
IS - 2
ER -