Edinburgh Research Explorer

Formalising Term Synthesis for Isacosy

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

Related Edinburgh Organisations

Access status

Open

Original languageEnglish
Title of host publicationWorkshop on Automated Mathematical Theory Exploration (Automatheo)
PublisherAutomatheo - IJCAR 2010
StatePublished - 2010

Abstract

IsaCoSy is a theory formation system for inductive theories. It synthesises conjectures and uses the ones that can be proved to produce a background theory for a new formalisation within a proof assistant. We present a formal account of the algorithms implemented in the system, and prove their correctness. In particular, we show that IsaCoSy only produces irreducible terms, using constraints generated from the left-hand sides of a set of rewrite rules.

Download statistics

No data available

ID: 152151