Tech Reports Home Contact
Technical Report Series
Browse Reports
Information for Authors
Contact Details

Technical Report HW-MACS-TR-0107

Title An Enhanced GUI for the Tinker tool
Authors Pierre Le Bras (with contributions from Gudmund Grov and Yuhui Lin)
Date 2014-09-24
Abstract Tinker is a tool that implements the proof-strategy graph (PSGraph) formalism. Here, tactics are represented as nodes and are linked with each other with edges. Each tactic will consume goals on input edges and generate new sub-goals which are sent to the output edges. The tool is generic w.r.t. theorem provers, and currently supports Isabelle and ProofPower. Users will use the normal interface provided by the theorem proving system, with the additional support for creating and evaluating proof strategy using Tinker's GUI. Tinker is built on top of Quantomatic. The first version of the GUI was very limited and highly integrated with the Quantomatic GUI. This document presents a new version of the GUI with several new features; including support for hierarchies and mode guided evaluation. The new version is decoupled further from Quantomatic. It is the outcome of the employment of the first author on EPSRC platform grant EP/J001058/1 over the summer of 2014.
Group DSG
Email Technical Report's Administrator
|MACS Home| Top of the Page

Department of Computer Science, Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS, +44 (0) 131 4514152

Last Updated: 02 September 2003 Copyright Heriot-Watt University, Disclaimer