Modal satisfiability via SMT solving

Mostrar todas las versiones(2)

Fil: Areces, Carlos Eduardo. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina.

Guardado en:
Detalles Bibliográficos
Autores principales: Areces, Carlos Eduardo, Fontaine, Pascal, Merz, Stephan
Formato: submittedVersion bookPart
Lenguaje:Inglés
Publicado: 2021
Materias:
Lógica modal
SMT
Acceso en línea:http://hdl.handle.net/11086/22112
Aporte de:
Repositorio Digital Universitario (UNC) de Universidad Nacional de Córdoba
id I10-R141-11086-22112
record_format dspace
spelling I10-R141-11086-221122023-12-13T18:13:46Z Modal satisfiability via SMT solving Areces, Carlos Eduardo Fontaine, Pascal Merz, Stephan Lógica modal SMT info:eu-repo/semantics/submittedVersion Fil: Areces, Carlos Eduardo. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. Fil: Areces, Carlos Eduardo. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Fil: Fontaine, Pascal. Université de Lorraine; Francia. Fil: Fontaine, Pascal. National Institute for Research in Digital Science and Technology; Francia. Fil: Merz, Stephan. Université de Lorraine; Francia. Fil: Merz, Stephan. National Institute for Research in Digital Science and Technology; Francia. Modal logics extend classical propositional logic, and they are robustly decidable. Whereas most existing decision procedures for modal logics are based on tableau constructions, we propose a framework for obtaining decision procedures by adding instantiation rules to standard SAT and SMT solvers. Soundness, completeness, and termination of the procedures can be proved in a uniform and elementary way for the basic modal logic and some extensions. info:eu-repo/semantics/submittedVersion Fil: Areces, Carlos Eduardo. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina. Fil: Areces, Carlos Eduardo. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Fil: Fontaine, Pascal. Université de Lorraine; Francia. Fil: Fontaine, Pascal. National Institute for Research in Digital Science and Technology; Francia. Fil: Merz, Stephan. Université de Lorraine; Francia. Fil: Merz, Stephan. National Institute for Research in Digital Science and Technology; Francia. Ciencias de la Computación 2021-12-22T18:58:41Z 2021-12-22T18:58:41Z 2015 bookPart http://hdl.handle.net/11086/22112 eng Attribution-NonCommercial-NoDerivatives 4.0 International http://creativecommons.org/licenses/by-nc-nd/4.0/ Impreso
institution Universidad Nacional de Córdoba
institution_str I-10
repository_str R-141
collection Repositorio Digital Universitario (UNC)
language Inglés
topic Lógica modal
SMT
spellingShingle Lógica modal
SMT
Areces, Carlos Eduardo
Fontaine, Pascal
Merz, Stephan
Modal satisfiability via SMT solving
topic_facet Lógica modal
SMT
description Fil: Areces, Carlos Eduardo. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía y Física; Argentina.
format submittedVersion
bookPart
author Areces, Carlos Eduardo
Fontaine, Pascal
Merz, Stephan
author_facet Areces, Carlos Eduardo
Fontaine, Pascal
Merz, Stephan
author_sort Areces, Carlos Eduardo
title Modal satisfiability via SMT solving
title_short Modal satisfiability via SMT solving
title_full Modal satisfiability via SMT solving
title_fullStr Modal satisfiability via SMT solving
title_full_unstemmed Modal satisfiability via SMT solving
title_sort modal satisfiability via smt solving
publishDate 2021
url http://hdl.handle.net/11086/22112
work_keys_str_mv AT arecescarloseduardo modalsatisfiabilityviasmtsolving
AT fontainepascal modalsatisfiabilityviasmtsolving
AT merzstephan modalsatisfiabilityviasmtsolving
_version_ 1806949663227510784

Ejemplares similares