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

(13)

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

Describes a project that uses

Uses Software

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

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)