Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC (Q5195279): Difference between revisions

Latest revision as of 16:18, 30 December 2024

scientific article; zbMATH DE number 7106513

Language	Label	Description	Also known as
English	Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC	scientific article; zbMATH DE number 7106513

Statements

0 references

0 references

0 references

0 references

18 September 2019

0 references

full work available at URL

https://arxiv.org/abs/1610.05593

0 references

zbMATH Keywords

proof maintenance

0 references

theorem proving

0 references

graphical tactic language

0 references

describes a project that uses

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

0 references

MaRDI publication profile

0 references

title

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

0 references

cites work

Refactoring Proofs with Tactician

0 references

Now f is continuous (exercise

0 references

Jape: A calculator for animating proof-on-paper

0 references

Q3838801

0 references

Q4499291

0 references

Theorem Proving in Higher Order Logics

0 references

Open-graphs and monoidal theories

0 references

Fundamentals of algebraic graph transformation

0 references

The Four Colour Theorem: Engineering of a Formal Proof

0 references

Edinburgh LCF. A mechanized logic of computation

0 references

A Graphical Language for Proof Strategies

0 references

HOL Light: An Overview

0 references

The Zipper

0 references

Interactive Simplifier Tracing and Debugging in Isabelle

0 references

Quantomatic: A Proof Assistant for Diagrammatic Reasoning

0 references

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

0 references

A higher-order implementation of rewriting

0 references

A Brief Overview of HOL4

0 references

Towards Formal Proof Script Refactoring

0 references

Polar: A Framework for Proof Refactoring

0 references

Identifiers

zbMATH Open document ID

1451.68324

0 references

Mathematics Subject Classification ID

0 references

0 references

0 references

0 references

0 references

10.6092/ISSN.1972-5787/6298

0 references

Sitelinks

Mathematics(1 entry)

mardi Publication:5195279

@@ label / en / label / en @@
+Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
@@ Property / DOI @@
-.6092/issn.1972-5787/6298
@@ Property / DOI: 10.6092/issn.1972-5787/6298 / rank @@
-Normal rank
@@ Property / describes a project that uses @@
+Jape
@@ Property / describes a project that uses: Jape / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/Isar
@@ Property / describes a project that uses: Isabelle/Isar / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL Light
@@ Property / describes a project that uses: HOL Light / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+OpenTheory
@@ Property / describes a project that uses: OpenTheory / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+kepler98
@@ Property / describes a project that uses: kepler98 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Tactician
@@ Property / describes a project that uses: Tactician / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+LOUI
@@ Property / describes a project that uses: LOUI / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+XIsabelle
@@ Property / describes a project that uses: XIsabelle / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2536147106
@@ Property / OpenAlex ID: W2536147106 / rank @@
+Normal rank
@@ Property / title @@
+Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC (English)
+Normal rank
@@ Property / arXiv ID @@
+.05593
@@ Property / arXiv ID: 1610.05593 / rank @@
+Normal rank
@@ Property / cites work @@
+Refactoring Proofs with Tactician
@@ Property / cites work: Refactoring Proofs with Tactician / rank @@
+Normal rank
@@ Property / cites work @@
+Now f is continuous (exercise
@@ Property / cites work: Now f is continuous (exercise / rank @@
+Normal rank
@@ Property / cites work @@
+Jape: A calculator for animating proof-on-paper
@@ Property / cites work: Jape: A calculator for animating proof-on-paper / rank @@
+Normal rank
@@ Property / cites work @@
+Q3838801
@@ Property / cites work: Q3838801 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4499291
@@ Property / cites work: Q4499291 / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Open-graphs and monoidal theories
@@ Property / cites work: Open-graphs and monoidal theories / rank @@
+Normal rank
@@ Property / cites work @@
+Fundamentals of algebraic graph transformation
@@ Property / cites work: Fundamentals of algebraic graph transformation / rank @@
+Normal rank
@@ Property / cites work @@
+The Four Colour Theorem: Engineering of a Formal Proof
+Normal rank
@@ Property / cites work @@
+Edinburgh LCF. A mechanized logic of computation
@@ Property / cites work: Edinburgh LCF. A mechanized logic of computation / rank @@
+Normal rank
@@ Property / cites work @@
+A Graphical Language for Proof Strategies
@@ Property / cites work: A Graphical Language for Proof Strategies / rank @@
+Normal rank
@@ Property / cites work @@
+HOL Light: An Overview
@@ Property / cites work: HOL Light: An Overview / rank @@
+Normal rank
@@ Property / cites work @@
+The Zipper
@@ Property / cites work: The Zipper / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive Simplifier Tracing and Debugging in Isabelle
+Normal rank
@@ Property / cites work @@
+Quantomatic: A Proof Assistant for Diagrammatic Reasoning
+Normal rank
@@ Property / cites work @@
+Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
+Normal rank
@@ Property / cites work @@
+A higher-order implementation of rewriting
@@ Property / cites work: A higher-order implementation of rewriting / rank @@
+Normal rank
@@ Property / cites work @@
+A Brief Overview of HOL4
@@ Property / cites work: A Brief Overview of HOL4 / rank @@
+Normal rank
@@ Property / cites work @@
+Towards Formal Proof Script Refactoring
@@ Property / cites work: Towards Formal Proof Script Refactoring / rank @@
+Normal rank
@@ Property / cites work @@
+Polar: A Framework for Proof Refactoring
@@ Property / cites work: Polar: A Framework for Proof Refactoring / rank @@
+Normal rank
@@ Property / DOI @@
+.6092/ISSN.1972-5787/6298
@@ Property / DOI: 10.6092/ISSN.1972-5787/6298 / rank @@
+Normal rank