A Tableau Calculus for Hájek's Logic BL

MONTAGNA F;PINNA, GIOVANNI MICHELE;TIEZZI E. B. P.

2003-01-01

---

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.