A Tactic Language for Hiproofs

DOI10.1007/978-3-540-85110-3_30MaRDI QIDQ5505516zbMATH OpenOpenAlexFDO

Authors Ewen Denney, Christoph Lüth, D. Aspinall

Publication date 27 January 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-85110-3_30

Mathematics Subject Classification ID

Recommendations

• Tactics for hierarchical proof
• Hiproofs: a hierarchical notion of proof tree
• Capturing hiproofs in HOL light
• A tactic calculus. --- Abridged version
• A Proof-Theoretic Approach to Tactics

Cites work

• ArcAngel: a tactic language for refinement
• Dependent types ensure partial correctness of theorem provers
• Hiproofs: a hierarchical notion of proof tree
• scientific article; zbMATH DE number 1696760 (Why is no real title available?)
• Tinycals: step by step tacticals

Cited in

(5)

• Capturing hiproofs in HOL light
• Hiproofs: a hierarchical notion of proof tree
• A semantic basis for proof queries and transformations
• scientific article; zbMATH DE number 3870643 (Why is no real title available?)
• Tactics for hierarchical proof

Describes a project that uses

Uses Software

• ArcAngel

This page was built for publication: A Tactic Language for Hiproofs

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