52 citations · 79 across the 16 of their papers we have counts for
4 papers · 1 filter
Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
Yuhui Lin, Gudmund Grov, Rob Arthan
The use of a functional language to implement proof strategies as proof tactics in interactive theorem provers, often provides short, concise and elegant implementations. Whilst be…
Tinker, tailor, solver, proof
Gudmund Grov, Aleks Kissinger, Yuhui Lin
We introduce Tinker, a tool for designing and evaluating proof strategies based on proof-strategy graphs, a formalism previously introduced by the authors. We represent proof strat…
Towards Automated Proof Strategy Generalisation
Gudmund Grov, Ewen Maclean
The ability to automatically generalise (interactive) proofs and use such generalisations to discharge related conjectures is a very hard problem which remains unsolved. Here, we d…
A Graphical Language for Proof Strategies
Gudmund Grov, Aleks Kissinger, Yuhui Lin
Complex automated proof strategies are often difficult to extract, visualise, modify, and debug. Traditional tactic languages, often based on stack-based goal propagation, make it…