ProofScript: proof scripting for the masses

DOI10.1007/978-3-319-46750-4_19MaRDI QIDQ3179409zbMATH OpenOpenAlexFDO

Authors Steven Obua, Phil Scott, Jacques D. Fleuriot

Publication date 21 December 2016

Published in Theoretical Aspects of Computing – ICTAC 2016 (Search for Journal in Brave)

Full work available at URL https://www.pure.ed.ac.uk/ws/files/28382045/main.pdf

Mathematics Subject Classification ID

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

Recommendations

• Collaborative Interactive Theorem Proving with Clide
• scientific article; zbMATH DE number 1629953
• Communicating formal proofs: the case of Flyspeck
• A proof-centric approach to mathematical assistants
• Towards Formal Proof Script Refactoring

Cites work

• scientific article; zbMATH DE number 2185680 (Why is no real title available?)
• An Isabelle proof method language
• Edinburgh LCF. A mechanized logic of computation
• Partizan Games in Isabelle/HOLZF
• Set theory for verification. I: From foundations to functions
• Set theory for verification. II: Induction and recursion
• The next 700 programming languages
• Type inference for ZFH

Cited in

(1)

• ProofScript

Describes a project that uses

Uses Software

• ProofPeer
• Eisbach
• Isabelle/ZF
• Isar

This page was built for publication: ProofScript: proof scripting for the masses

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