Por favor, use este identificador para citar o enlazar a este item:
http://hdl.handle.net/10261/130394
COMPARTIR / EXPORTAR:
SHARE BASE | |
Visualizar otros formatos: MARC | Dublin Core | RDF | ORE | MODS | METS | DIDL | DATACITE | |
Título: | SAT and SMT technology for many-valued logics |
Autor: | Ansotegui, Carlos; Bofill, Miquel; Manyà, Felip CSIC ORCID ; Villaret, Mateu | Palabras clave: | Bit vectors Lukasiewicz infinitely-valued logic SMT SAT Regular encodings Many-valued logic Linear integer arithmetic Linear real arithmetic |
Fecha de publicación: | 2015 | Editor: | Old City Publishing | Citación: | Journal of Multiple-Valued Logic and Soft Computing 24: 151- 172 (2015) | Resumen: | © 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. | URI: | http://hdl.handle.net/10261/130394 | Identificadores: | issn: 1542-3980 |
Aparece en las colecciones: | (IIIA) Artículos |
Ficheros en este ítem:
Fichero | Descripción | Tamaño | Formato | |
---|---|---|---|---|
accesoRestringido.pdf | 15,38 kB | Adobe PDF | Visualizar/Abrir |
CORE Recommender
Page view(s)
186
checked on 17-abr-2024
Download(s)
58
checked on 17-abr-2024
Google ScholarTM
Check
NOTA: Los ítems de Digital.CSIC están protegidos por copyright, con todos los derechos reservados, a menos que se indique lo contrario.