Edinburgh Research Explorer

The Tinker GUI for Graphical Proof Strategies (tool demo)

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

Related Edinburgh Organisations

Open Access permissions

Open

Original languageEnglish
Title of host publicationProceedings of the Third Workshop on Formal Integrated Development Environment
PublisherOpen Publishing Association
Pages98-101
Number of pages3
StatePublished - 8 Nov 2016
EventThird Workshop on Formal Integrated Development Environment - St Raphael Resort, Cyprus
Duration: 8 Nov 20168 Nov 2016
http://fm2016.cs.ucy.ac.cy/workshops.html

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherOpen Publishing Association
Volume240
ISSN (Electronic)2075-2180

Conference

ConferenceThird Workshop on Formal Integrated Development Environment
Abbreviated titleF-IDE 2016
CountryCyprus
Period8/11/168/11/16
Internet address

Abstract

Most interactive theorem provers provide users with a tactic language in which they can encode common proof strategies in order to reduce user interaction. To encode proof strategies, these languages typically provide: a set of functions, called tactics, which reduce sub-goals into smaller and simpler sub-goals; and a set of combinators, called tacticals, which combines tactics in different ways.
Composition in most tacticals either relies on the number and the order of sub-goals, or tries all tactics on all sub-goals. The former is brittle as the number and the order could be changed if any of the sub-tactics changes; and the latter is hard to debug and maintain, as if a proof fails the actual position is hard to find. It is also difficult for others to see the intuition behind tactic design.

Event

Third Workshop on Formal Integrated Development Environment

8/11/168/11/16

Cyprus

Event: Conference

ID: 41133212