A Tableau Calculus for Hajek's Logic BL

Abstract
We introduce a tableau calculus for Háajek'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 Γ is polynomial in the number of symbols of Γ. As a corollary we obtain an alternative proof of Co‐NP completeness of BL.

This publication has 0 references indexed in Scilit: