Three tactic theorem proving

DOI10.1007/3-540-48256-3_14MaRDI QIDQ4945208zbMATH OpenFDO

Authors Don Syme

Publication date 23 March 2000

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

Full work available at URL https://doi.org/10.1007/3-540-48256-3_14

zbMATH Keywords

DECLAREtheorem prover

Mathematics Subject Classification ID

Recommendations

• A tactic language for declarative proofs
• scientific article; zbMATH DE number 1863397
• Tactic theorem proving with refinement-tree proofs and metavariables
• A synthesis of the procedural and declarative styles of interactive theorem proving
• scientific article; zbMATH DE number 2177623

Cited in

(9)

• Semantics of Mizar as an Isabelle object logic
• Improving legibility of formal proofs based on the close reference principle is NP-hard
• A Brief Overview of Mizar
• A Declarative Language for the Coq Proof Assistant
• scientific article; zbMATH DE number 1927421 (Why is no real title available?)
• On the implementation of an extensible declarative proof language
• scientific article; zbMATH DE number 970721 (Why is no real title available?)
• A tactic language for declarative proofs
• A proof-centric approach to mathematical assistants

Describes a project that uses

Uses Software

• Mizar

This page was built for publication: Three tactic theorem proving

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