Edinburgh Research Explorer

The Tinker tool for graphical tactic development

Research output: Contribution to journalArticle

Related Edinburgh Organisations

Open Access permissions

Open

Documents

  • Download as Adobe PDF

    Final published version, 2 MB, PDF-document

    Licence: Creative Commons: Attribution (CC-BY)

https://link.springer.com/article/10.1007%2Fs10009-017-0452-7
Original languageEnglish
Pages (from-to)1-17
Number of pages17
JournalInternational Journal on Software Tools for Technology Transfer
Early online date17 Mar 2017
DOIs
StateE-pub ahead of print - 17 Mar 2017

Abstract

PSGraph (Grov et al. in LPAR. Springer, Berlin, pp 324--339, 2013) is a graphical language to support the development and maintenance of proof tactics for interactive theorem provers. By using labelled hierarchical graphs this formalisation improves upon analysis and maintenance found in traditional tactic languages. Tool support for PSGraph is achieved by Tinker (Grov et al. in UITP 2014, ENTCS, vol 167. Open Publishing Association, London, pp 23--34, 2014; Lin et al. in Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 573--579, 2016): a theorem prover-independent system, which is connected to several different provers, with a graphical user interface including novel features to develop and debug proof tactics graphically. In this paper we provide a detailed and formal account of PSGraph and show how theorem prover independence is achieved by Tinker. We then show practical use of PSGraph and Tinker by developing several proof patterns using the language and tool.

Download statistics

No data available

ID: 41133107