Heterogeneous Proofs: Spider Diagrams Meet Higher-Order Provers

DOI10.1007/978-3-642-22863-6_29zbMath1342.68305OpenAlexW2255432097WikidataQ62046880 ScholiaQ62046880MaRDI QIDQ3088023

Matej Urbas, Mateja Jamnik

Publication date: 17 August 2011

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

Full work available at URL: https://doi.org/10.1007/978-3-642-22863-6_29

Mathematics Subject Classification ID

Related Items (2)

Proof theory for heterogeneous logic combining formulas and diagrams: proof normalization ⋮ Towards a Proof Theory for Heterogeneous Logic Combining Sentences and Diagrams

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• Dr.Doodle
• Openproof

Cites Work

• On automating diagrammatic proofs of arithmetic arguments
• Reasoning with sentences and diagrams
• Edinburgh LCF. A mechanized logic of computation
• Automated theorem proving in Euler diagram systems
• On the Completeness of Spider Diagrams Augmented with Constants
• The Isabelle Framework
• Heterogeneous Reasoning and Its Logic
• Automated Reasoning
• Spider Diagrams

This page was built for publication: Heterogeneous Proofs: Spider Diagrams Meet Higher-Order Provers