A tool for studying inhabitation of simple types

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.