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.