We introduce a tableau calculus for Hajek'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.
Montagna, F., Pinna, G.M., Tiezzi, E.B.P. (2003). A tableau calculus for Hajek’s logic BL. JOURNAL OF LOGIC AND COMPUTATION, 13(2), 241-259 [10.1093/logcom/13.2.241].
A tableau calculus for Hajek’s logic BL
MONTAGNA, FRANCO;PINNA, GIOVANNI MICHELE;TIEZZI, ELISA BENEDETTA PRIMAVERA
2003-01-01
Abstract
We introduce a tableau calculus for Hajek'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.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
https://hdl.handle.net/11365/3550
Attenzione
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo