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.
A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications / M. Ferrari, C. Fiorentini, G. Fiorino. - In: JOURNAL OF APPLIED NON-CLASSICAL LOGICS. - ISSN 1166-3081. - 19:2(2009), pp. 149-166. [10.3166/jancl.19.149-166]
A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications
C. Fiorentini;
2009
Abstract
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.
| File | Dimensione | Formato | |
|---|---|---|---|
|
2009_jancl.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
174.4 kB
Formato
Adobe PDF
|
174.4 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
