The Tinker GUI for Graphical Proof Strategies (tool demo)

Gudmund Grov, Yuhui Lin, Pierre Le Bras

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

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.
Original languageEnglish
Title of host publicationProceedings of the Third Workshop on Formal Integrated Development Environment
PublisherOpen Publishing Association
Pages98-101
Number of pages3
Publication statusPublished - 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
Country/TerritoryCyprus
Period8/11/168/11/16
Internet address

Fingerprint

Dive into the research topics of 'The Tinker GUI for Graphical Proof Strategies (tool demo)'. Together they form a unique fingerprint.

Cite this