November 24, 2014

What is MikiBeta?

Proof trees are useful. We use proof trees for type checking as well as proofs in deductive systems. However, it is often tedious to write proof trees by hand. Proof trees tend to require a large space; we have to rewrite metavariables whenever unification occurs.

MikiBeta is a general GUI library for visualizing proof trees. It enables us to construct a proof tree on a computer, taking care of large space and rewriting via unification. Here are two examples of the GUI, ported to run on a browser. Input a term, press go, click the term, and press a button. But really nice thing about MikiBeta is that it enables us to have such GUI for any proof systems. It works as follows. We first provide the definition of a proof system. MikiBeta then processes it and produces a GUI for that particular proof system. It is awfully useful!


Tested environment: MacOSX 10.6, OCaml 3.12.0


How to Execute



This document was translated from LATEX by HEVEA.