scientific article; zbMATH DE number 1424018

MaRDI QIDQ4945208zbMATH OpenFDO

Authors Don Syme

Publication date 23 March 2000

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?)
• scientific article; zbMATH DE number 1424017 (Why is no real title available?)
• 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:

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