Edinburgh Research Explorer

Scheme-Based Synthesis of Inductive Theories

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Related Edinburgh Organisations

Access status

Open

Documents

http://www.springerlink.com/content/m885557421m7418m/
Original languageEnglish
Title of host publicationAdvances in Artificial Intelligence
Subtitle of host publication9th Mexican International Conference on Artificial Intelligence, MICAI 2010, Pachuca, Mexico, November 8-13, 2010, Proceedings, Part I
EditorsGrigori Sidorov, Arturo Hernández Aguirre, Carlos Alberto Reyes García
PublisherSpringer-Verlag GmbH
Pages348-361
Number of pages14
ISBN (Print)978-3-642-16760-7
DOIs
StatePublished - 2010

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
Volume6437
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

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.

Research areas

  • Mathematical theory exploration, schemes, theorem proving, termination, term rewriting

Download statistics

No data available

ID: 449718