A tableau for set-satisfiability for extended fuzzy logic BL

TL;DR

This paper introduces a tableau calculus for extended fuzzy logic BL, enabling the determination of models for set-satisfiable formulas involving additional connectives, thus generalizing previous BL tableau methods.

Contribution

It extends the tableau calculus for BL to handle an extended fuzzy logic with Baaz connective and involutive negation, allowing for model existence checks for sets of formulas.

Findings

Provides a method to find models for extended BL formulas.

Enables checking validity across all continuous t-norms.

Offers a decision procedure for set-satisfiability in extended fuzzy logic.

Abstract

This paper presents a tableau calculus for finding a model for a set-satisfiable finite set of formulas of an extended fuzzy logic BL, a fuzzy logic BL with additional Baaz connective and the involutive negation, if such a model exists. The calculus is a generalisation of a tableau calculus for BL, which is based on the decomposition theorem for a continuous t-norm. The aforementioned tableau calculus for BL is used to prove that a formula A of the extended BL is valid with respect to all continuous t-norms or to find a continuous t-norm * and assignment V of propositional atoms to [0,1] such that *-evaluation V*(A)<1. The tableau calculus presented in this paper enables for a finite set of formulas F of the extended BL and a subset K of [0,1] to find a continuous t-norm * and assignment V of propositional atoms to [0,1] such that *-evaluation V*(A) belongs to K for all formulas A that belong to F, or alternatively to show that such a model does not exist.