##
A Tableau Calculus for BL

### Agnieszka Kulacka

In this talk I present a tableau calculus for BL. After providing an
informal description of the calculus, I will demonstrate the
refutational procedure and the search for models procedure on selected
examples. The idea of the calculus is based on the converse of the
consequence of the Decomposition Theorem for a continuous t-norm, by
which this operation is shown to be equivalent to the ordinal sum of a
family of t-norms defined on countably many intervals. In the paper
Tableau Calculus for Basic Fuzzy Logic BL I only show that closing a
tableau for a formula is equivalent to showing validity of the formula
with respect to LP-norms (a type of continuous t-norms). Now, we can
also show that a formula is valid with respect to every continuous
t-norm. In the approach presented here, however, we use Theorem 3 of
Complexity of t-tautologies by Baaz, Hajek, Montagna and Veith, which
says that if a formula is a tautology of the ordinal sum of all finite
families of Lukasiewicz t-norms, then it is valid. Therefore, we will
only need to use Branch Expansion Rules based on the Lukasiewicz t-norm
and its residuum.