Merging Procedural and Declarative Proof

DOI10.1007/978-3-642-02444-3_13MaRDI QIDQ3638254zbMATH OpenOpenAlexWikidataFDO

Authors Cezary Kaliszyk, Freek Wiedijk

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) Structure of proofs (03F07) Grammars and rewriting systems (68Q42)

Recommendations

• A synthesis of the procedural and declarative styles of interactive theorem proving
• Simplifying proofs in Fitch-style natural deduction systems
• scientific article; zbMATH DE number 1863397
• Presentation of proofs in modal natural deduction
• scientific article; zbMATH DE number 1927421

Cites work

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

Cited in

(6)

• Semantics of Mizar as an Isabelle object logic
• A synthesis of the procedural and declarative styles of interactive theorem proving
• scientific article; zbMATH DE number 1927421 (Why is no real title available?)
• scientific article; zbMATH DE number 1863397 (Why is no real title available?)
• Reconstructing proofs at the assertion level
• Simplifying proofs in Fitch-style natural deduction systems

Describes a project that uses

Uses Software

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

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

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