IRIS - Institutional Research Information System
IRIS è il sistema di gestione integrata dei dati della ricerca (persone, progetti, pubblicazioni, attività) adottato dall'Università degli Studi dell’Insubria.
IRInSubria - Institutional Repository Insubria
IRInSubria raccoglie, conserva, documenta e dissemina le informazioni sulla produzione scientifica dell'Università degli Studi dell’Insubria anche ai fini della valutazione della ricerca.
EnglishSince 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.
| Autori: | |
| Data di pubblicazione: | 2009 |
| Titolo: | A Tableau Calculus for Propositional Intuitionistic Logic with a Refined Treatment of Nested Implications |
| Rivista: | JOURNAL OF APPLIED NON-CLASSICAL LOGICS |
| Codice identificativo Scopus: | 2-s2.0-84880065004 |
| Parole Chiave: | Intuitionistic Propositional Logic; tableau calculi; decision procedures |
| Appare nelle tipologie: | Articolo su Rivista |
File in questo prodotto:
Copyright © 2018