Name
Abstract | ||
|---|---|---|
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 β-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. |
Year | DOI | Venue |
|---|---|---|
2002 | 10.1016/S1571-0661(04)80545-0 | Electronic Notes in Theoretical Computer Science |
Keywords | Field | DocType |
implicational logic,provability,uniqueness of proofs,formula-tree approach | Intuitionistic logic,Uniqueness,Discrete mathematics,Mathematical proof,Corollary,Mathematics | Journal |
Volume | ISSN | Citations |
67 | 1571-0661 | 1 |
PageRank | References | Authors |
0.40 | 1 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sabine Broda | 1 | 64 | 13.83 |
| Lu ís Damas | 2 | 128 | 22.34 |