© 2003 by Oxford University Press
Original Article |
A Tableau Calculus for Hájek's Logic BL
1 Dipartimento di Matematica, Via del Capitano 15, 53100 Siena, Italy. E-mail: montagna{at}unisi.itpinna{at}unisi.ittiezzie{at}unisi.it
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.
Keywords: Fuzzy logics; tableau calculus; proof systems
Received 26 March 2001.