English   español  
Please use this identifier to cite or link to this item: http://hdl.handle.net/10261/136837
logo share SHARE logo core CORE   Add this article to your Mendeley library MendeleyBASE

Visualizar otros formatos: MARC | Dublin Core | RDF | ORE | MODS | METS | DIDL | DATACITE
Exportar a otros formatos:


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

AuthorsAnsotegui, Carlos; Bofill, Miquel; Manyà, Felip CSIC ORCID ; Villaret, Mateu
Multiple-valued logics
Automated theorem provers
Issue Date2016
CitationFuzzy Sets and Systems 292: 32- 48 (2016)
AbstractThere is a relatively large number of papers dealing with complexity and proof theory issues of multiple-valued logics. Nevertheless, little attention has been paid so far to the development of efficient and robust solvers for such logics. In this paper we investigate how the technology of Satisfiability Modulo Theories (SMT) can be effectively used to build efficient automated theorem provers for relevant finitely-valued and infinitely-valued logics, taking the logics of Łukasiewicz, Gödel and Product as case studies. Besides, we report on an experimental investigation that evaluates the performance of SMT technology when solving multiple-valued logic problems, and compares the finitely-valued solvers for Łukasiewicz and Gödel logics with their infinitely-valued solvers from a computational point of view. We also compare the performance of SMT technology and MIP technology when testing the satisfiability on a genuine family of multiple-valued clausal forms.
Identifiersdoi: 10.1016/j.fss.2015.04.011
issn: 0165-0114
Appears in Collections:(IIIA) Artículos
Files in This Item:
File Description SizeFormat 
accesoRestringido.pdf15,38 kBAdobe PDFThumbnail
Show full item record
Review this work

Related articles:

WARNING: Items in Digital.CSIC are protected by copyright, with all rights reserved, unless otherwise indicated.