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

From MaRDI portal
Changed an Item
Normalize DOI.
 
(6 intermediate revisions by 4 users not shown)
Property / DOI
 
Property / DOI: 10.1016/j.fss.2015.04.011 / rank
Normal rank
 
Property / describes a project that uses
 
Property / describes a project that uses: Yices / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: z3 / rank
 
Normal rank
Property / describes a project that uses
 
Property / describes a project that uses: NiBLoS / rank
 
Normal rank
Property / MaRDI profile type
 
Property / MaRDI profile type: MaRDI publication profile / rank
 
Normal rank
Property / full work available at URL
 
Property / full work available at URL: https://doi.org/10.1016/j.fss.2015.04.011 / rank
 
Normal rank
Property / OpenAlex ID
 
Property / OpenAlex ID: W2040193103 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Complexity issues in Basic Logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Resolution-based theorem proving for many-valued logics / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2701980 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q2757760 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Mathematical Fuzzy Logics / rank
 
Normal rank
Property / cites work
 
Property / cites work: Metamathematics of fuzzy logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Proof theory for fuzzy logics / rank
 
Normal rank
Property / cites work
 
Property / cites work: Short Conjunctive Normal Forms in Finitely Valued Logics / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3184605 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Logic for Programming, Artificial Intelligence, and Reasoning / rank
 
Normal rank
Property / cites work
 
Property / cites work: Tableaux for Łukasiewicz infinite-valued logic / rank
 
Normal rank
Property / cites work
 
Property / cites work: Satisfiability checking in Łukasiewicz logic as finite constraint satisfaction / rank
 
Normal rank
Property / cites work
 
Property / cites work: Many-valued logic and mixed integer programming / rank
 
Normal rank
Property / cites work
 
Property / cites work: On the structure of semi-groups on a compact manifold with boundary / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3506045 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q4512929 / rank
 
Normal rank
Property / DOI
 
Property / DOI: 10.1016/J.FSS.2015.04.011 / rank
 
Normal rank

Latest revision as of 04:30, 11 December 2024

scientific article
Language Label Description Also known as
English
Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers
scientific article

    Statements

    Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers (English)
    0 references
    0 references
    0 references
    0 references
    0 references
    19 February 2018
    0 references
    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.
    0 references
    multiple-valued logics
    0 references
    automated theorem provers
    0 references
    SMT
    0 references
    benchmarks
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references

    Identifiers