'The Tinker' for Rodin

Yibo Liang; Yuhui Lin; Gudmund Grov

doi:10.1007/978-3-319-33600-8_19

'The Tinker' for Rodin

Yibo Liang, Yuhui Lin^*, Gudmund Grov

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

4 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 language	English
Title of host publication	Abstract State Machines, Alloy, B, TLA, VDM, and Z
Subtitle of host publication	5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings
Editors	M. Butler, K.-D. Schewe, A. Mashkoor, M. Biro
Publisher	Springer
Pages	262-268
Number of pages	7
ISBN (Electronic)	9783319336008
ISBN (Print)	9783319335995
DOIs	https://doi.org/10.1007/978-3-319-33600-8_19
Publication status	Published - 2016
Event	5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z 2016 - Linz, Australia Duration: 23 May 2016 → 27 May 2016

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer international Publishing
Volume	9675
ISSN (Print)	0302-9743

Conference

Conference	5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z 2016
Country/Territory	Australia
City	Linz
Period	23/05/16 → 27/05/16

Access to Document

10.1007/978-3-319-33600-8_19

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. https://doi.org/10.1007/978-3-319-33600-8_19

@inproceedings{dc9c1bb7c22e4c7ea1fbb0abf1084d96,

title = "'The Tinker' for Rodin",

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.",

author = "Yibo Liang and Yuhui Lin and Gudmund Grov",

year = "2016",

doi = "10.1007/978-3-319-33600-8\_19",

language = "English",

isbn = "9783319335995",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "262--268",

editor = "M. Butler and K.-D. Schewe and A. Mashkoor and M. Biro",

booktitle = "Abstract State Machines, Alloy, B, TLA, VDM, and Z",

note = "5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z 2016 ; Conference date: 23-05-2016 Through 27-05-2016",

}

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. Lecture Notes in Computer Science, vol. 9675, Springer, pp. 262-268, 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z 2016, Linz, Australia, 23/05/16. https://doi.org/10.1007/978-3-319-33600-8_19

'The Tinker' for Rodin. / Liang, Yibo; Lin, Yuhui; Grov, Gudmund.
Abstract State Machines, Alloy, B, TLA, VDM, and Z: 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings. ed. / M. Butler; K.-D. Schewe; A. Mashkoor; M. Biro. Springer, 2016. p. 262-268 (Lecture Notes in Computer Science; Vol. 9675).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - 'The Tinker' for Rodin

AU - Liang, Yibo

AU - Lin, Yuhui

AU - Grov, Gudmund

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/84978696162

U2 - 10.1007/978-3-319-33600-8_19

DO - 10.1007/978-3-319-33600-8_19

M3 - Conference contribution

SN - 9783319335995

T3 - Lecture Notes in Computer Science

SP - 262

EP - 268

BT - Abstract State Machines, Alloy, B, TLA, VDM, and Z

A2 - Butler, M.

A2 - Schewe, K.-D.

A2 - Mashkoor, A.

A2 - Biro, M.

PB - Springer

T2 - 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z 2016

Y2 - 23 May 2016 through 27 May 2016

ER -

'The Tinker' for Rodin

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this