15 DEZEMBRO / SEXTA FEIRA / 23:29
FCUP PT 
 EN
 
 
APRESENTAÇÃO
PESSOAS
ENSINO
INVESTIGAÇÃO
BIBLIOTECA
NOTÍCIAS
CONTACTOS

Technical Report: DCC-2004-01

The Formula-Tree Proof Method

Sabine Broda and Luís Damas

DCC-FC & LIACC, Universidade do Porto
R. do Campo Alegre 823, 4150-180 Porto, Portugal
Phone: 351 22 6078830, Fax: 351 22 6003654
E-mail: {sbb,luis}@ncc.up.pt
January 2004

Abstract

We define an alternative representation for types in the simply typed $\lambda$-calculus or equivalently for formulas in the implicational fragment of intuitionist propositional logic, which gives us a better insight on the nature of a types structure and its relation to the structure of the set of its normal inhabitants. Based on this representation of a type $\varphi$, called its formula-tree, we define the notion of a valid proof-tree. Any such valid proof-tree represents a finite set of normal inhabitants of $\varphi$ and every normal inhabitant corresponds to exactly one valid proof-tree, constructable with the primitive parts in the formula-tree of $\varphi$. Precise algorithms are given to establish this relation. This method can be used to easily recognize and prove results concerning inhabitation/provability.


FCUP 2017