Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers (Q1697332): Difference between revisions

Many-valued (propositional) logics have been studied for many years and important examples are the logics by Gödel and Łukasiewicz, which come as logics with finitely many or infinitely many truth values, for instance, as finitely many integer values, or as rational values between 0 and 1 (both included) in the finite case, or as all the real numbers in the interval \([0,1]\) in the infinite case. The connectives are defined, for instance, in Gödel logics, so that conjunction corresponds to the minimum and disjunction to the maximum function. In addition to these two families of logics, the paper studies product logic in which the truth value of conjunction is defined as the product of the component values. Properties and calculi for such logics have been studied since the early 20th century. More towards the end of the 20th century actual theorem provers have been developed. The authors study the application of general purpose SMT solvers as theorem provers for these many valued logics. SMT solvers are satisfiability modulo theories solvers and have successfully been used in many areas. The authors give straightforward translations from problems of many-valued logics to formulations readable by SMT solvers. Essentially, each propositional logic variable can take only one of the different truth values, the connectives correspond to functions on numbers, and the formulae are translated into arithmetic expressions. Then, satisfiability is checked. If no model is found then the formulae are unsatisfiable. The efficiency of the approach is tested with respect to certain benchmark problems and different encodings are compared. The tests are done for finite numbers of truth values from 3 through 21 with 5 to 50 variables. For some tests with infinite logics, the number of variables is 500. The general approach has a very good performance. The usual pattern of SAT solvers is reproduced that with a small number or a high number of clauses the problem is typically easily shown to be solvable or unsolvable, respectively; and that in the transition area between solvability and unsolvability the computational complexity is high.