Visual theorem proving with the Incredible Proof Machine

DOI10.1007/978-3-319-43144-4_8zbMATH Open1478.68435OpenAlexW2488236528MaRDI QIDQ2829254FDOQ2829254

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

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

Mathematics Subject Classification ID

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

Cites Work

• Binders unbound
• A rewriting calculus for multigraphs with ports

Cited In (12)

• Visualising reasoning: what ATP can learn from CP
• ProofViz: an interactive visual proof explorer
• Title not available (Why is that?)
• 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

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)