Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers
type: Item
instance of: scholarly article
title: Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers
zbMATH Open document ID: 1387.03007
author: Carlos Ansótegui
author: Miquel Bofill
author: Felip Manya
author: Mateu Villaret
published in: Fuzzy Sets and Systems
publication date: 2018-02-19T00:00:00Z
review text: 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 sho…
reviewed by: Manfred Kerber
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B50
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 6840665
zbMATH Keywords: multiple-valued logics
zbMATH Keywords: automated theorem provers
zbMATH Keywords: SMT
zbMATH Keywords: benchmarks
describes a project that uses: SMT-LIB
describes a project that uses: GLPK
describes a project that uses: Yices
describes a project that uses: z3
describes a project that uses: NiBLoS
MaRDI profile type: Publication
full work available at URL: j.fss.2015.04.011
OpenAlex ID: W2040193103
cites work: Complexity issues in Basic Logic
cites work: Resolution-based theorem proving for many-valued logics
cites work: The SAT problem of signed CNF formulas
cites work: A treatise on many-valued logics
cites work: Mathematical Fuzzy Logics
cites work: Metamathematics of fuzzy logic
cites work: Proof theory for fuzzy logics
cites work: Short Conjunctive Normal Forms in Finitely Valued Logics
cites work: Q3184605
cites work: Logic for Programming, Artificial Intelligence, and Reasoning
cites work: Tableaux for Łukasiewicz infinite-valued logic
cites work: Satisfiability checking in Łukasiewicz logic as finite constraint satisfaction
cites work: Many-valued logic and mixed integer programming
cites work: On the structure of semi-groups on a compact manifold with boundary
cites work: Q3506045
cites work: Q4512929
DOI: 10.1016/J.FSS.2015.04.011
Recommended article: Automated deduction for many-valued logics
Recommended article: Q4289327
Recommended article: Q4380155
Recommended article: A framework for automated reasoning in multiple-valued logics
Recommended article: An application of automated equational reasoning to many-valued logic
Recommended article: Q4212163
Recommended article: Q3726086
Recommended article: Q4544342
Recommended article: Resolution-based theorem proving for many-valued logics
Recommended article: Automatic theorem proving in paraconsistent logics: Theory and implementation
description: scientific article; zbMATH DE number 6840665