We introduce a tableau calculus for Haíek’s Basic Logic BL. This calculus has many of the desirable properties of a proof system: it is cut-free, it has the subformula property, correctness of proof can be checked in P-time, and the number of symbols in any branch of the reduction tree of any sequent Gamma is polynomial in the number of symbols of Gamma. As a corollary we obtain an alternative proof of  co-NP completeness of BL.
A Tableau Calculus for Hájek's Logic BL / Montagna, F., Pinna, G.M., Tiezzi, E.B.P.. - In: JOURNAL OF LOGIC AND COMPUTATION. - ISSN 0955-792X. - 13:2(2003), pp. 241-259.
A Tableau Calculus for Hájek's Logic BL
PINNA, GIOVANNI MICHELE;
2003
Abstract
We introduce a tableau calculus for Haíek’s Basic Logic BL. This calculus has many of the desirable properties of a proof system: it is cut-free, it has the subformula property, correctness of proof can be checked in P-time, and the number of symbols in any branch of the reduction tree of any sequent Gamma is polynomial in the number of symbols of Gamma. As a corollary we obtain an alternative proof of  co-NP completeness of BL.File allegati a 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.
