English   español  
Please use this identifier to cite or link to this item: http://hdl.handle.net/10261/130394
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:


SAT and SMT technology for many-valued logics

AuthorsAnsotegui, Carlos ; Bofill, Miquel; Manyà, Felip CSIC ORCID ; Villaret, Mateu
KeywordsBit vectors
Lukasiewicz infinitely-valued logic
Regular encodings
Many-valued logics
Linear integer arithmetic
Linear real arithmetic
Issue Date2015
PublisherOld City Publishing
CitationJournal of Multiple-Valued Logic and Soft Computing 24: 151- 172 (2015)
Abstract© 2014 Old City Publishing, Inc. We propose to use the SAT and SMT technology to deal with manyvalued logics. Our approach is twofold. Firstly, we focus on finitelyvalued logics, and extend the language of signed CNF formulas with linear integer arithmetic constraints. This way, we get a simple modeling language in which a wide range of practical combinatorial problems admit compact and natural encodings. We then define efficient translations from our language into the SAT and SMT formalisms, and propose to use SAT and SMT solvers for finding solutions. Secondly, we show how we can use the SMT technology to build efficient automated theorem provers for infinitely-valued logics, taking Lukasiewicz infinitely-valued logic as a case study.
Identifiersissn: 1542-3980
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

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