November 24, 2014
What is MikiBeta?
Proof trees are useful.
We use proof trees for type checking as well as proofs in deductive
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
It is awfully useful!
Tested environment: MacOSX 10.6, OCaml 3.12.0
- X11 that can display UTF characters.
How to Execute
Go to miki directory and execute make bcl.
- Go to one of the example directories and execute make.
- Launch the GUI by executing ./go.
(You might want to enter something like
env LANG=ja_JP.UTF-8 ./go.)
- Read AST.txt for the accepted syntax.
Sakurai, K., and K. Asai
``MikiBeta: A General GUI Library for Visualizing Proof Trees,"
20th International Symposium on Logic-Based Program Synthesis and
Transformation (LOPSTR '10), pp. 184-193 (July 2010).
Post conference version in
pp. 84-98 (April 2011).
This document was translated from LATEX by