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.
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 language | English |
---|---|
Title of host publication | Proceedings of the Third Workshop on Formal Integrated Development Environment |
Publisher | Open Publishing Association |
Pages | 98-101 |
Number of pages | 3 |
Publication status | Published - 8 Nov 2016 |
Event | Third Workshop on Formal Integrated Development Environment - St Raphael Resort, Cyprus Duration: 8 Nov 2016 → 8 Nov 2016 http://fm2016.cs.ucy.ac.cy/workshops.html |
Publication series
Name | Electronic Proceedings in Theoretical Computer Science |
---|---|
Publisher | Open Publishing Association |
Volume | 240 |
ISSN (Electronic) | 2075-2180 |
Conference
Conference | Third Workshop on Formal Integrated Development Environment |
---|---|
Abbreviated title | F-IDE 2016 |
Country/Territory | Cyprus |
Period | 8/11/16 → 8/11/16 |
Internet address |