A tactic language for declarative proofs

DOI10.1007/978-3-642-14052-5_9MaRDI QIDQ5747644zbMATH OpenOpenAlexFDO

Authors Serge Autexier, Dominik Dietrich

Publication date 14 September 2010

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14052-5_9

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 1424018
• scientific article; zbMATH DE number 1863397
• scientific article; zbMATH DE number 1104384
• A synthesis of the procedural and declarative styles of interactive theorem proving
• Declarative representation of proof terms

Cited in

(7)

• Declarative representation of proof terms
• A synthesis of the procedural and declarative styles of interactive theorem proving
• A Declarative Language for the Coq Proof Assistant
• Using the TPTP Language for Writing Derivations and Finite Interpretations
• scientific article; zbMATH DE number 1863397 (Why is no real title available?)
• scientific article; zbMATH DE number 1424017 (Why is no real title available?)
• scientific article; zbMATH DE number 1424018 (Why is no real title available?)

Describes a project that uses

Uses Software

• Stratego
• IsaPlanner
• Isar
• Mizar
• SAD

This page was built for publication: A tactic language for declarative proofs

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