'The Tinker' for Rodin

Yibo Liang, Yuhui Lin, Gudmund Grov

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

3 Citations (Scopus)

Abstract

PSGraph [3] is a graphical proof strategy language, which uses the formalisation of labelled hierarchical graphs to provide support for the development and maintenance of large and complex proof tactics. PSGraph has been implemented as the Tinker system, which previously supported the Isabelle and ProofPower theorem provers [4]. In this paper we present a Rodin version of Tinker, which allows Rodin users to encode, analyse and debug their proof strategies in Tinker.

Original languageEnglish
Title of host publicationAbstract State Machines, Alloy, B, TLA, VDM, and Z
Subtitle of host publication5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings
EditorsM. Butler, K.-D. Schewe, A. Mashkoor, M. Biro
PublisherSpringer International Publishing
Pages262-268
Number of pages7
ISBN (Electronic)9783319336008
ISBN (Print)9783319335995
DOIs
Publication statusPublished - 2016
Event5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z 2016 - Linz, Australia
Duration: 23 May 201627 May 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer international Publishing
Volume9675
ISSN (Print)0302-9743

Conference

Conference5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z 2016
CountryAustralia
CityLinz
Period23/05/1627/05/16

Cite this

Liang, Y., Lin, Y., & Grov, G. (2016). 'The Tinker' for Rodin. In M. Butler, K-D. Schewe, A. Mashkoor, & M. Biro (Eds.), Abstract State Machines, Alloy, B, TLA, VDM, and Z: 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings (pp. 262-268). (Lecture Notes in Computer Science; Vol. 9675). Springer International Publishing. https://doi.org/10.1007/978-3-319-33600-8_19