Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 A tool for studying inhabitation of simple types 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
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.