## Incredible Proof Machine

swMATH ID: | 28840 |

Software Authors: | Joachim Breitner; Denis Lohner |

Description: | The meta theory of the Incredible Proof Machine. 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. |

Homepage: | https://www.isa-afp.org/entries/Incredible_Proof_Machine.html |

Dependencies: | Isabelle |

Related Software: | Isabelle/HOL; FOL_Harrison; Propositional Resolution; Abstract Soundness; Verified Prover; Lambda Free RPOs; Archive Formal Proofs; Incompleteness Theorems; FOL Fitting; Abstract Completeness; Knuth Bendix Orders; Paraconsistency; Superposition Calculus; Completeness theorem; GitHub; GRAT; theoremprover-museum; IsaFoL; Jitawa; E Theorem Prover |

Referenced in: | 2 Publications |

### Referenced by 2 Authors

1 | Breitner, Joachim |

1 | Schlichtkrull, Anders |

### Referenced in 1 Serial

1 | Journal of Automated Reasoning |

### Referenced in 2 Fields

2 | Mathematical logic and foundations (03-XX) |

2 | Computer science (68-XX) |