An SMT-based solver for continuous t-norm based logics

Abstract

In the literature, little attention has been paid to the development of solvers for systems of mathematical fuzzy logic, even though there is an important number of studies on complexity and proof theory for them. In this paper, extending a recent approach by Ansótegui et al., we present ongoing work on an efficient and modular SMT-based solver for a wide family of continuous t-norm based fuzzy logics. The solver is able to deal with most famous fuzzy logics (including BL, Łukasiewicz, Gödel and Product); and for each of them, it is able to test, among others, satisfiability, tautologicity and logical consequence problems. Note that, unlike the classical case, these problems are not in general interdefinable in fuzzy logics. Some empirical results are reported at the end of the paper. © 2012 Springer-Verlag.