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].

A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications

FIORINO, GUIDO GIUSEPPE
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..
No
Articolo in rivista - Articolo scientifico
Scientifica
Decision procedures; Intuitionistic Propositional Logic; Tableau calculi;
English
149
166
18
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].
Ferrari, M; Fiorentini, C; Fiorino, G
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/10281/7922
Citazioni
  • Scopus 4
  • ???jsp.display-item.citation.isi??? ND
Social impact