**Sabine Broda, Luís Damas
DCC LIACC, Universidade do Porto
e-mail: {sbb,luis}@ncc.up.pt
**

The *Formula Tree Lab* is a tool for studying inhabitation of
simple types. It has been developed at LIACC &
DCC, University of Porto, and is based on the formula-tree proof
method first introduced in [2].
In this user-friendly environment

- one can easily build proof-trees for simple types;
- in parallel, during the construction of a proof-tree, a scheme for long normal inhabitants is automatically constructed, and after completion the corresponding (finite, non-empty) set of normal inhabitants may optionally be generated;
- an extra option allows for focusing on principal inhabitants;
- conversely one can check if a normal term is an inhabitant of a type and construct the corresponding proof-tree.

The main purpose of this tool is to visualize the straight relationship that exists between the structure of a type and the structure of its normal inhabitants. In fact, a lot of properties and results concerning inhabitation of simple types, or equivalently concerning provability in the implicational fragment of intuitionistic logic, cf. subsection 3, become straightforward with this approach.

- How to use the
*Formula Tree Lab*- Constructing proof-trees and normal inhabitants
- Construction of proof-trees from normal inhabitants
- Principal Inhabitants

- Formula Tree Lab Applet
- Short description of the formula-tree proof method
- Formula-trees
- Proof-trees
- The relationship between proof-trees and normal inhabitants of simple types

- A sample result based on the analysis of the formula-tree of a type
- Bibliography
- Troubleshooting
- About this document ...