Edinburgh Research Explorer

Tinker, Tailor, Solver, Proof

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

Related Edinburgh Organisations

Open Access permissions

Open

Documents

  • Download as Adobe PDF

    Final published version, 455 KB, PDF-document

    Licence: Creative Commons: Attribution (CC-BY)

https://arxiv.org/abs/1410.8217
Original languageEnglish
Title of host publicationIn Proceedings of Eleventh Workshop on User Interfaces for Theorem Provers (UITP 2014)
PublisherOpen Publishing Association
Pages23-34
Number of pages12
DOIs
Publication statusPublished - 2014

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
Volume167
ISSN (Print)2075-2180

Abstract

We introduce Tinker, a tool for designing and evaluating proof strategies based on proof-strategy graphs, a formalism previously introduced by the authors. We represent proof strategies as open-graphs, which are directed graphs with additional input/output edges. Tactics appear as nodes in a graph, and can be `piped' together by adding edges between them. Goals are added to the input edges of such a graph, and flow through the graph as the strategy is evaluated. Properties of the edges ensure that only the right `type' of goals are accepted. In this paper, we detail the Tinker tool and show how it can be integrated with two different theorem provers: Isabelle and ProofPower.

Download statistics

No data available

ID: 41181840