Since 1993, when Hudelmaier developed an O(n log n)-space decision procedure for propositional Intuitionistic Logic, a lot of work has been done to improve the efficiency of the related proof-search algorithms. In this paper a tableau calculus using the signs T, F and Fc with a new set of rules to treat signed formulas of the kind T((A → B) → C) is provided. The main feature of the calculus is the reduction of both the non-determinism in proof-search and the width of proofs with respect to Hudelmaier's one. These improvements have a significant influence on the performances of the implementation..
Ferrari, M., Fiorentini, C., & Fiorino, G. (2009). A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications. JOURNAL OF APPLIED NON-CLASSICAL LOGICS, 19(2), 149-166 [10.3166/jancl.19.149-166].
Citazione: | Ferrari, M., Fiorentini, C., & Fiorino, G. (2009). A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications. JOURNAL OF APPLIED NON-CLASSICAL LOGICS, 19(2), 149-166 [10.3166/jancl.19.149-166]. | |
Tipo: | Articolo in rivista - Articolo scientifico | |
Carattere della pubblicazione: | Scientifica | |
Presenza di un coautore afferente ad Istituzioni straniere: | No | |
Titolo: | A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications | |
Autori: | Ferrari, M; Fiorentini, C; Fiorino, G | |
Autori: | ||
Data di pubblicazione: | 2009 | |
Lingua: | English | |
Rivista: | JOURNAL OF APPLIED NON-CLASSICAL LOGICS | |
Digital Object Identifier (DOI): | http://dx.doi.org/10.3166/jancl.19.149-166 | |
Appare nelle tipologie: | 01 - Articolo su rivista |