Merging Procedural and Declarative Proof

DOI10.1007/978-3-642-02444-3_13zbMath1246.68198OpenAlexW1589866633WikidataQ108482194 ScholiaQ108482194MaRDI QIDQ3638254

Freek Wiedijk, Cezary Kaliszyk

Publication date: 2 July 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-642-02444-3_13

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Structure of proofs (03F07)

Related Items (1)

Semantics of Mizar as an Isabelle object logic

Uses Software

• Coq
• Isabelle/Isar
• PVS
• Isar
• Mizar
• ProofWeb

Cites Work

• Linear logic
• Mathematical knowledge management in HELM
• Logic in Computer Science
• From Deduction Graphs to Proof Nets: Boxes and Sharing in the Graphical Presentation of Deductions
• Rewriting Techniques and Applications

This page was built for publication: Merging Procedural and Declarative Proof