Ítem


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

There 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

Research partially supported by the Generalitat de Catalunya grant AGAUR 2014-SGR-118, and the Ministerio de Economía y Competitividad projects CO-PRIVACY TIN2011-27076-C03-03, TASSAT-2 TIN2013-48031-C4-4-P and HeLo TIN2012-33042. The third author was supported by Mobility Grant PRX14/00195 of the Ministerio de Educación, Cultura y Deporte

Elsevier

Director: Ministerio de Economía y Competitividad (Espanya)
Autor: Ansótegui, Carlos
Bofill Arasa, Miquel
Manyà, Felip
Villaret i Ausellé, Mateu
Data: 1 juny 2016
Resum: There 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
Research partially supported by the Generalitat de Catalunya grant AGAUR 2014-SGR-118, and the Ministerio de Economía y Competitividad projects CO-PRIVACY TIN2011-27076-C03-03, TASSAT-2 TIN2013-48031-C4-4-P and HeLo TIN2012-33042. The third author was supported by Mobility Grant PRX14/00195 of the Ministerio de Educación, Cultura y Deporte
Format: application/pdf
Accés al document: http://hdl.handle.net/10256/12739
Llenguatge: eng
Editor: Elsevier
Col·lecció: info:eu-repo/semantics/altIdentifier/doi/10.1016/j.fss.2015.04.011
info:eu-repo/semantics/altIdentifier/issn/0165-0114
info:eu-repo/grantAgreement/MINECO//TIN2012-33042/ES/HERRAMIENTAS LOGICAS PARA PROBLEMAS COMBINATORIOS/
Drets: Tots els drets reservats
Matèria: Lògica matemàtica
Logic, Symbolic and mathematical
Teoremes -- Demostració automàtica
Automatic theorem proving
Títol: Automated theorem provers for multiple-valued logics with satisfiability modulo theory solvers
Tipus: info:eu-repo/semantics/article
Repositori: DUGiDocs

Matèries

Autors