Visual theorem proving with the Incredible Proof Machine

DOI10.1007/978-3-319-43144-4_8MaRDI QIDQ2829254zbMATH OpenOpenAlexFDO

Authors Joachim Breitner

Publication date 27 October 2016

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

Full work available at URL https://doi.org/10.1007/978-3-319-43144-4_8

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• ProofViz: an interactive visual proof explorer
• scientific article; zbMATH DE number 3922016
• scientific article; zbMATH DE number 1497860
• scientific article; zbMATH DE number 1231506
• Panoptes: an exploration tool for formal proofs

Cites work

• A rewriting calculus for multigraphs with ports
• Binders unbound

Cited in

(12)

• Visualising reasoning: what ATP can learn from CP
• ProofViz: an interactive visual proof explorer
• scientific article; zbMATH DE number 1479613 (Why is no real title available?)
• Interactive computer programs (ICP) for teaching the indirect method for theorem proving
• Formalization of the resolution calculus for first-order logic
• Verifying a sequent calculus Prover for first-order logic with functions in Isabelle/HOL
• Querying proofs
• Programming and verifying a declarative first-order prover in Isabelle/HOL
• SeCaV: a sequent calculus verifier in Isabelle/HOL
• Panoptes: an exploration tool for formal proofs
• VizAR: visualization of automated reasoning proofs (system description)
• Jape: a calculator for animating proof-on-paper

Describes a project that uses

Uses Software

• Logitext
• Incredible Proof Machine
• Unbound
• Isabelle/HOL
• Coq

This page was built for publication: Visual theorem proving with the Incredible Proof Machine

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