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

DOI10.6092/issn.1972-5787/6298zbMath1451.68324arXiv1610.05593OpenAlexW2536147106MaRDI QIDQ5195279

Yu-Hui Lin, Rob Arthan, Gudmund Grov

Publication date: 18 September 2019

Full work available at URL: https://arxiv.org/abs/1610.05593

zbMATH Keywords

theorem provinggraphical tactic languageproof maintenance

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

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

Uses Software

• Isabelle
• Isabelle/Isar
• IsaPlanner
• Isar
• HOL
• ProofPower
• HOL Light
• LCF
• Quantomatic
• Tactician
• LOUI
• kepler98
• XIsabelle
• Jape
• OpenTheory

Cites Work

• Unnamed Item
• Unnamed Item
• A higher-order implementation of rewriting
• Edinburgh LCF. A mechanized logic of computation
• Fundamentals of algebraic graph transformation
• A Graphical Language for Proof Strategies
• Polar: A Framework for Proof Refactoring
• HOL Light: An Overview
• Quantomatic: A Proof Assistant for Diagrammatic Reasoning
• A Brief Overview of HOL4
• The Four Colour Theorem: Engineering of a Formal Proof
• The Zipper
• Open-graphs and monoidal theories
• Refactoring Proofs with Tactician
• Now f is continuous (exercise
• Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
• Towards Formal Proof Script Refactoring
• Jape: A calculator for animating proof-on-paper
• Theorem Proving in Higher Order Logics
• Interactive Simplifier Tracing and Debugging in Isabelle

This page was built for publication: Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC