Free-variable semantic tableaux for the logic of fuzzy inequalities

We present a free-variable tableau calculus for the logic of fuzzy inequalities F$\forall$, which is an extension of infinite-valued first-order Lukasiewicz logic Ł$\forall$. The set of all Ł$\forall$-sentences provable in the hypersequent calculus of Baaz and Metcalfe for Ł$\forall$ is embedded into the set of all F$\forall$-sentences provable in the given tableau calculus. We prove NP-completeness of the problem of checking tableau closability and propose an algorithm, which is based on unification, for solving the problem.