Edinburgh Research Explorer

'The Tinker' for Rodin

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

Original languageEnglish
Title of host publicationAbstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings
PublisherSpringer, Cham
Pages262-268
Number of pages7
ISBN (Electronic)978-3-319-33600-8
ISBN (Print)978-3-319-33599-5
DOIs
Publication statusPublished - 11 May 2016
EventAbstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference - Linz, Austria
Duration: 23 May 201627 May 2016
https://dl.acm.org/citation.cfm?id=2990689&picked=prox

Publication series

NameLecture Notes in Computer Science
PublisherSpringer, Cham
Volume9675
ISSN (Print)0302-9743

Conference

ConferenceAbstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference
Abbreviated titleABZ 2016
CountryAustria
CityLinz
Period23/05/1627/05/16
Internet address

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.

Event

Download statistics

No data available

ID: 41132671