Visual Theorem Proving with the Incredible Proof Machine

DOI10.1007/978-3-319-43144-4_8zbMath1478.68435OpenAlexW2488236528MaRDI QIDQ2829254

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)

Related Items (2)

Formalization of the resolution calculus for first-order logic ⋮ Programming and verifying a declarative first-order prover in Isabelle/HOL

Uses Software

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

Cites Work

• Binders unbound
• A Rewriting Calculus for Multigraphs with Ports

This page was built for publication: Visual Theorem Proving with the Incredible Proof Machine