Refactoring proofs with Tactician

DOI10.1007/978-3-662-49224-6_6zbMATH Open1461.68246OpenAlexW2296387478MaRDI QIDQ4988643FDOQ4988643

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

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

Mathematics Subject Classification ID

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

Cited In (5)

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

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)