Studying provability in implicational intuitionistic logic: The formula tree approach

• Type: Article in International Conference Proceedings Book
• Date: 2002

Authors

Broda, S (Author) FCUP; Damas, L (Author) FCUP

Conference proceedings International

Title: Electronic Notes in Theoretical Computer Science

Pages: 135-151

WoLLIC'2002, 9th Workshop on Logic, Language, Information and Computation

Rio de Janeiro, 30 July 2002 through 2 August 2002

Indexing

ISI Web of Knowledge

Scopus - 2 Citations

Other information

Authenticus ID: P-007-D7G

DOI: 10.1016/s1571-0661(04)80545-0

Abstract (EN): We use an alternative graphical representation for formulas in implicational intuitionistic logic in order to obtain and demonstrate results concerning provability. We demonstrate the adequateness of the method in this area, showing that one can easily recognize and prove new results and simplify the proofs of others. As such, we extend a known class of formulas for which uniqueness of ß-¿-normal proofs is true and define a new one for uniqueness of beta-normal proofs. We also give a precise characterization of the set of provable monatomic formulas and obtain as a corollary a necessary condition for intuitionistic theorems in general. ©2002 Published by Elsevier Science B.V.

Language: English

Type (Professor's evaluation): Scientific

No. of pages: 17