### Abstract

The Incredible Proof Machine is an interactive visual theorem prover which represents proofs as port graphs. We model this proof representation in Isabelle, and prove that it is just as powerful as natural deduction.

### License

BSD License

### Topics

- Logic/Proof theory

### Session Incredible_Proof_Machine

- Indexed_FSet
- Abstract_Formula
- Incredible_Signatures
- Incredible_Deduction
- Abstract_Rules
- Abstract_Rules_To_Incredible
- Entailment
- Natural_Deduction
- Incredible_Correctness
- Rose_Tree
- Incredible_Trees
- Build_Incredible_Tree
- Incredible_Completeness
- Incredible_Everything
- Propositional_Formulas
- Incredible_Propositional
- Incredible_Propositional_Tasks
- Predicate_Formulas
- Incredible_Predicate
- Incredible_Predicate_Tasks

### Depends on

- Abstract Completeness

## Cite

×

Incredible_Proof_Machine-AFP

    @article{Incredible_Proof_Machine-AFP,
      author  = {Joachim Breitner and Denis Lohner},
      title   = {The meta theory of the Incredible Proof Machine},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Incredible_Proof_Machine.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- May 20, 2016 : Isabelle2016