Refactoring Proofs with Tactician

DOI10.1007/978-3-662-49224-6_6zbMath1461.68246OpenAlexW2296387478MaRDI QIDQ4988643

No author found.

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)

Related Items (2)

TacticToe: learning to prove with tactics ⋮ Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC

Uses Software

• HOL Light
• Tactician

This page was built for publication: Refactoring Proofs with Tactician