Modal satisfiability via SMT solving

Mostrar todas las versiones(2)

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....

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Areces, Carlos Eduardo, Fontaine, Pascal, Merz, Stephan
Formato: bookPart submittedVersion
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
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 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.
format bookPart
submittedVersion
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
bdutipo_str Repositorios
_version_ 1764820392084504579

Ejemplares similares