Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction)
We present a coinductive definition of models for modal logics and show that it provides a homogeneous framework in which it is possible to include different modal languages ranging from classical modalities to operators from hybrid and memory logics. Moreover, results that had to be proved separate...
Guardado en:
| Publicado: |
2010
|
|---|---|
| Materias: | |
| Acceso en línea: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_15708683_v8_n4_p305_Areces http://hdl.handle.net/20.500.12110/paper_15708683_v8_n4_p305_Areces |
| Aporte de: |
| id |
paper:paper_15708683_v8_n4_p305_Areces |
|---|---|
| record_format |
dspace |
| spelling |
paper:paper_15708683_v8_n4_p305_Areces2023-06-08T16:24:16Z Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction) Hybrid logics Modal depth Modal logics Normal forms Bisimulations Coinduction Conjunctive normal forms Hybrid logic Modal depth Modal formulas Modal language Modal logic Normal form Polynomial-time Propositional logic Satisfiability Polynomial approximation Boolean functions We present a coinductive definition of models for modal logics and show that it provides a homogeneous framework in which it is possible to include different modal languages ranging from classical modalities to operators from hybrid and memory logics. Moreover, results that had to be proved separately for each different language-but whose proofs were known to be mere routine-now can be proved in a general way. We show, for example, that we can have a unique definition of bisimulation for all these languages, and prove a single invariance-under-bisimulation theorem. We then use the new framework to investigate normal forms for modal logics. The normal form we introduce may have a smaller modal depth than the original formula, and it is inspired by global modalities like the universal modality and the satisfiability operator from hybrid logics. These modalities can be extracted from under the scope of other operators. We provide a general definition of extractable modalities and show how to compute extracted normal forms. As it is the case with other classical normal forms-e.g., the conjunctive normal form of propositional logic-the extracted normal form of a formula can be exponentially bigger than the original formula, if we require the two formulas to be equivalent. If we only require equi-satisfiability, then every modal formula has an extracted normal form which is only polynomially bigger than the original formula, and it can be computed in polynomial time. © 2010 Elsevier B.V. 2010 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_15708683_v8_n4_p305_Areces http://hdl.handle.net/20.500.12110/paper_15708683_v8_n4_p305_Areces |
| institution |
Universidad de Buenos Aires |
| institution_str |
I-28 |
| repository_str |
R-134 |
| collection |
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) |
| topic |
Hybrid logics Modal depth Modal logics Normal forms Bisimulations Coinduction Conjunctive normal forms Hybrid logic Modal depth Modal formulas Modal language Modal logic Normal form Polynomial-time Propositional logic Satisfiability Polynomial approximation Boolean functions |
| spellingShingle |
Hybrid logics Modal depth Modal logics Normal forms Bisimulations Coinduction Conjunctive normal forms Hybrid logic Modal depth Modal formulas Modal language Modal logic Normal form Polynomial-time Propositional logic Satisfiability Polynomial approximation Boolean functions Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction) |
| topic_facet |
Hybrid logics Modal depth Modal logics Normal forms Bisimulations Coinduction Conjunctive normal forms Hybrid logic Modal depth Modal formulas Modal language Modal logic Normal form Polynomial-time Propositional logic Satisfiability Polynomial approximation Boolean functions |
| description |
We present a coinductive definition of models for modal logics and show that it provides a homogeneous framework in which it is possible to include different modal languages ranging from classical modalities to operators from hybrid and memory logics. Moreover, results that had to be proved separately for each different language-but whose proofs were known to be mere routine-now can be proved in a general way. We show, for example, that we can have a unique definition of bisimulation for all these languages, and prove a single invariance-under-bisimulation theorem. We then use the new framework to investigate normal forms for modal logics. The normal form we introduce may have a smaller modal depth than the original formula, and it is inspired by global modalities like the universal modality and the satisfiability operator from hybrid logics. These modalities can be extracted from under the scope of other operators. We provide a general definition of extractable modalities and show how to compute extracted normal forms. As it is the case with other classical normal forms-e.g., the conjunctive normal form of propositional logic-the extracted normal form of a formula can be exponentially bigger than the original formula, if we require the two formulas to be equivalent. If we only require equi-satisfiability, then every modal formula has an extracted normal form which is only polynomially bigger than the original formula, and it can be computed in polynomial time. © 2010 Elsevier B.V. |
| title |
Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction) |
| title_short |
Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction) |
| title_full |
Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction) |
| title_fullStr |
Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction) |
| title_full_unstemmed |
Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction) |
| title_sort |
coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction) |
| publishDate |
2010 |
| url |
https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_15708683_v8_n4_p305_Areces http://hdl.handle.net/20.500.12110/paper_15708683_v8_n4_p305_Areces |
| _version_ |
1768543391176458240 |