The meta theory of the Incredible Proof Machine

 

Title: The meta theory of the Incredible Proof Machine
Authors: Joachim Breitner and Denis Lohner
Submission date: 2016-05-20
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.
BibTeX:
@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{http://isa-afp.org/entries/Incredible_Proof_Machine.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Abstract_Completeness