next up previous
Next: How to use the

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

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.




next up previous
Next: How to use the
Sabine Broda