The meta theory of the Incredible Proof Machine

Joachim Breitner 🌐 and Denis Lohner 🌐

May 20, 2016

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

Session Incredible_Proof_Machine

Depends on

Cite

× 
@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: