Refactoring proofs with Tactician

DOI10.1007/978-3-662-49224-6_6MaRDI QIDQ4988643zbMATH OpenOpenAlexFDO

Authors

Publication date 18 May 2021

Published in Software Engineering and Formal Methods (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-662-49224-6_6

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Towards Formal Proof Script Refactoring
• The Tactician. A seamless, interactive tactic learner and prover for Coq
• A Proof-Theoretic Approach to Tactics
• An overview of the Tecton proof system
• Tactic theorem proving with refinement-tree proofs and metavariables

Cited in

(6)

• TacticToe: learning to prove with tactics
• The Tactician. A seamless, interactive tactic learner and prover for Coq
• \textsc{Polar}: a framework for proof refactoring
• Using CafeOBJ to mechanise refactoring proofs and application
• Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
• Supporting maintenance of formal mathematics with similarity search

Describes a project that uses

Uses Software

• HOL Light
• Tactician

This page was built for publication: Refactoring proofs with Tactician

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4988643)