Basic Logic, SMT solvers and finitely generated varieties of GBL-algebras

Basic Logic was introduced by Petr Hájek to provide a unified approach to fuzzy logics, and judging by its rapid adoption in the research community, it has enjoyed considerable success in this regard. One of the reasons is that while it is a very general logic, it has elegant semantics with respect to the real unit interval, which allow for practical applications and use of standard software tools. Here we show how to use these semantics to encode propositional Basic Logic into the Satisfiability Modulo Theories (SMT) framework, based on an interpretation of Lukasiewicz logic, Gödel logic and product logic into SMT [4]. Ultimately these ideas go back to Mundici’s result [13] that satisfiablity for Lukasiewicz logic is NP-complete, and Hähnle’s translation from Lukasiewicz logic to integer linear programming [8, 9]. In the current setting the translation to SMT is very simple, and since there are several efficient SMT-solvers available, this is probably one of the most effective and flexible ways of implementing a decision procedure for propositional basic logic. Basic logic algebras (or BL-algebras for short) are bounded integral commutative residuated lattices that satisfy divisibility and prelinearity. The latter property implies that subdirectly irreducible BL-algebras are linearly ordered. Generalized BL-algebras (or GBL-algebras) are just divisible residuated lattices, but still retain many of the properties of BL-algebras. For example they have distributive lattice reducts, the fusion operation distributes over the meet operation, and in the n-potent case they are integral and commutative [10]. The subdirectly irreducible GBL-algebras are no longer linearly ordered, but in the finite case they have a well-understood structure theory based on the so-called poset product construction [10, 11]