





Technical Report: DCC200401The FormulaTree Proof MethodSabine Broda and Luís DamasR. do Campo Alegre 823, 4150180 Porto, Portugal Phone: 351 22 6078830, Fax: 351 22 6003654 Email: {sbb,luis}@ncc.up.pt AbstractWe 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 formulatree, we define the notion of a valid prooftree. Any such valid prooftree represents a finite set of normal inhabitants of $\varphi$ and every normal inhabitant corresponds to exactly one valid prooftree, constructable with the primitive parts in the formulatree of $\varphi$. Precise algorithms are given to establish this relation. This method can be used to easily recognize and prove results concerning inhabitation/provability. 

