OUP > Journals > Computing/Engineer. & Mathematics/Stats. > Journal of Logic and Computation
Journal of Logic and Computation
Volume 13, Issue 2, April 2003: pp. 241259
A Tableau Calculus for Hájek's Logic BL
Franco Montagna^{1}, G. Michele Pinna^{1} and Elisa B. P. Tiezzi^{1}
^{1}Dipartimento di Matematica, Via del Capitano 15, 53100 Siena, Italy. Email: {montagna,pinna,tiezzie}@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 cutfree, it has the subformula property, correctness of proof can be checked in Ptime, and the number of symbols in any branch of the reduction tree of any sequent [Ggr] is polynomial in the number of symbols of [Ggr]. As a corollary we obtain an alternative proof of CoNP completeness of BL.
Keywords: Fuzzy logics; tableau calculus; proof systems
Table of Contents
FullText PDF (188 KB)
