MikiBeta
February 27, 2018
-
Important notice:
Please refer to the
new MikiBeta page.
- Below is the old version that corresponds to the LOPSTER 2010
paper.
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!
Requirements
-
OCaml
- X11 that can display UTF characters.
Tested environment: MacOSX 10.6, OCaml 3.12.0
Download
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.
Publication
-
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).
abstract,
pdf.
Post conference version in
LNCS 6564,
pp. 84-98 (April 2011).
Members
This document was translated from LATEX by
HEVEA.