bonsai - prooftrees in natural deduction

Version 0.1 (beta). Release April 7th 2004.

bonsai is an interactive, graphical system to create, manipulate and display prooftrees (from typed lambda terms).

bonsai might be interesting to you if you study or teach the basics of proof theory in mathematical logic (to students of mathematics or computer science). Or if you just want to see prooftrees. (The screenshots below should help you decide if the program is something for you.)


bonsai is written in perl with the graphical extension perl-Tk. So you need perl and perl-Tk. Bonsai was tested with Linux, but it might run with other operation systems, too.

You also need a color display with at least 14 inch (for now), and a reasonable strong processor.
The code consists of several modules, and is about 120 K in size. The archive below also contains some example files and a manual in pdf format.


Bonsai is free software. See the README for the licence. Version 0.1 was developed by me mainly in March 2004 at the Institute of Mathematics, University of Munich.


Here are some screenshots:
Startframe
A simple prooftree found with 'search'
The same tree with a different way of displaying formulae
Contents of an example file (with 'actice/clickable' formulae)
Lambda term of a longer proof. Prooftree can be reconstructed from this
Sturcture of a large prooftree, displayed with a very small font
Some stage in Statman's example showing that the Complete Discharge Convention isn't always the right thing
First order example: Robinson Arithmetic as read in from a text file


The following gziped tape archive contains the code, examples files and a manual.

Bonsai 0.1

Instructions for GNU/Linux users:

Make a directory (e.g., bonsai) which will contain the program and cd to it, e.g.,

mkdir bonsai
cd bonsai/

 Download the archive to that directory.

Unzip and unpack it:

gunzip bonsai_0.1.tar.gz
tar -xvf bonsai_0.1.tar
chmod 755 bonsai.pl (if necessary - doesn't hurt)

If you have perl and perl-Tk installed, you can start bonsai with

bonsai.pl
 or
perl bonsai.pl
(The first version should work if perl is in /usr/bin/perl.)
Try perl ./bonsai.pl otherwise.)

There is also a README.txt file which you might look at.

The manual - a pdf.file - is in the directory "manual".

cd manual/
xpdf manual.pdf (or: acroread manual.pdf ).

It might be useful to print it. There is a step by step quick start example which covers much of what you will use all the time (at least for propositional logic).