Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers

DOI10.1016/j.fss.2015.04.011zbMath1387.03007OpenAlexW2040193103MaRDI QIDQ1697332

Carlos Ansótegui, Mateu Villaret, Miquel Bofill, Felip Manyà

Publication date: 19 February 2018

Published in: Fuzzy Sets and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.fss.2015.04.011

zbMATH Keywords

benchmarksSMTautomated theorem proversmultiple-valued logics

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Many-valued logic (03B50)

Related Items (4)

On generalized hoops, homomorphic images of residuated lattices, and (G)BL-algebras ⋮ Editorial ⋮ New complexity results for Łukasiewicz logic ⋮ The Complexity of 3-Valued Łukasiewicz Rules

Uses Software

• SMT-LIB
• Yices
• GLPK
• z3
• NiBLoS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Satisfiability checking in Łukasiewicz logic as finite constraint satisfaction
• On the structure of semi-groups on a compact manifold with boundary
• Complexity issues in Basic Logic
• Metamathematics of fuzzy logic
• Tableaux for Łukasiewicz infinite-valued logic
• Resolution-based theorem proving for many-valued logics
• Many-valued logic and mixed integer programming
• Proof theory for fuzzy logics
• Mathematical Fuzzy Logics
• Short Conjunctive Normal Forms in Finitely Valued Logics
• Logic for Programming, Artificial Intelligence, and Reasoning

This page was built for publication: Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers