English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

The use of a functional language to implement proof strategies as prooftactics in interactive theorem provers, often provides short, concise andelegant implementations. Whilst being elegant, the use of higher order featuresand combinator languages often results in a very procedural view of a strategy,which may deviate significantly from the high-level ideas behind it. This canmake a tactic hard to understand and hence difficult to to debug and maintainfor experts and non-experts alike: one often has to tear apart complexcombinations of lower level tactics manually in order to analyse a failure inthe overall strategy. In an industrial technology transfer project, we havebeen working on porting a very large and complex proof tactic into PSGraph, agraphical language for representing proof strategies, supported by the Tinkertool. The goal of this work is to improve understandability and maintainabilityof tactics. Motivated by some initial successes with this, we here extendPSGraph with additional features for development and debugging. Through there-implementation and refactoring of several existing tactics, we demonstratesthe advantages of PSGraph compared with a typical linear (term-based) tacticlanguage with respect to debugging, readability and maintenance. In order toact as guidance for others, we give a fairly detailed comparison of the userexperience with the two approaches. The paper is supported by a web pageproviding further details about the implementation as well as interactiveillustrations of the examples.

Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC