Sabine Broda, Luís Damas
DCC LIACC, Universidade do Porto
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 . In this user-friendly environment
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.