Navegar

Colección

Datos Estadísticas

Artículo

Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

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.

Registro:

Documento: Artículo
Título:Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction)
Autor:Areces, C.; Gorín, D.
Filiación:INRIA Nancy Grand Est, Nancy, France
Departamento de Computación, Universidad de Buenos Aires, Buenos Aires, Argentina
Palabras clave: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
Año:2010
Volumen:8
Número:4
Página de inicio:305
Página de fin:318
DOI: http://dx.doi.org/10.1016/j.jal.2010.08.010
Título revista:Journal of Applied Logic
Título revista abreviado:J. Appl. Logic
ISSN:15708683
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_15708683_v8_n4_p305_Areces

Referencias:

  • Areces, C., Ten Cate, B., Hybrid Logics, (5), pp. 821-868. , P. Blackburn, et al
  • Areces, C., Figueira, D., Figueira, S., Mera, S., Expressive power and decidability for memory logics (2008) Lecture Notes in Computer Science, 5110, pp. 56-68. , Logic, Language, Information and Computation, Proceedings of WoLLIC 2008, Springer
  • Baaz, M., Egly, U., Leitsch, A., Normal Form Transformations, (18), pp. 273-333. , J. Robinson and A. Voronkov
  • Blackburn, P., De Rijke, M., Venema, Y., (2001) Modal Logic, , Cambridge University Press
  • (2006) Handbook of Modal Logics, , P. Blackburn, F. Wolter, J. van Benthem, Elsevier
  • DIMACS Satisfiability Suggested Format, , ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/doc,1993, lastvisited22/08/2009
  • Enjalbert, P., Fariñas Del Cerro, L., Modal resolution in clausal form (1989) Theoretical Computer Science, 65, pp. 1-33
  • Giunchiglia, F., Sebastiani, R., Building decision procedures for modal logics from propositional decision procedures: Case study of modal K (2008) Lecture Notes in Artificial Intelligence, 1104, pp. 583-597. , Proceedings of CADE-13, Springer
  • Giunchiglia, F., Sebastiani, R., A SAT-based decision procedure for ALC (1996) Principals of Knowledge Representation and Reasoning, Proceedings of the Fifth International Conference, KR'96, pp. 304-314
  • Giunchiglia, E., Tacchella, A., Giunchiglia, F., SAT-based decision procedures for classical modal logics (2002) Journal of Automated Reasoning, 28, pp. 143-171
  • Goranko, V., Passy, S., Using the universal modality: Gains and questions (1992) Journal of Logic and Computation, 2, pp. 5-30
  • Kurz, A., Coalgebras and their logics (2006) SIGACT News, 37, pp. 57-77
  • Ladner, R., The computational complexity of provability in systems of modal propositional logic (1977) SIAM Journal on Computing, 6, pp. 467-480
  • Mints, G., Resolution calculi for modal logics, in: Eight Papers Translated from the Russian (1989) American Mathematical Society Translations, 143, pp. 1-14. , AMS
  • Nguyen, L., On the complexity of fragments of modal logics (2004) Advances in Modal Logic, 5, pp. 249-268
  • Nonnengart, A., Weidenbach, C., Computing Small Clause Normal Forms, (18), pp. 335-366. , J. Robinson and A. Voronkov
  • Patel-Schneider, P., Sebastiani, R., A new general method to generate random modal formulae for testing decision procedures (2003) Journal of Artificial Intelligence Research, 18, pp. 351-389
  • (2001) Handbook of Automated Reasoning (2 Volumes), , J. Robinson, A. Voronkov, MIT Press/Elsevier
  • Tacchella, A., SAT system description Proceedings of the 1999 International Workshop on Description Logics, DL'99 July 30-August 1, , P. Lambrix, A. Borgida, M. Lenzerini, R. Möller, P. Patel-Schneider 1999 CEUR Workshop Proceedings vol. 22 1999 Linköping Sweden
  • Ten Cate, B., (2005) Model Theory for Extended Modal Languages, , PhD thesis, ILLC Dissertation Series DS-2005-01, University of Amsterdam
  • Van Der Hoek, W., De Rijke, M., Generalized quantifiers and modal logic (1993) Journal of Logic, Language and Information, 2, pp. 19-58

Citas:

---------- APA ----------
Areces, C. & Gorín, D. (2010) . Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction). Journal of Applied Logic, 8(4), 305-318.
http://dx.doi.org/10.1016/j.jal.2010.08.010
---------- CHICAGO ----------
Areces, C., Gorín, D. "Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction)" . Journal of Applied Logic 8, no. 4 (2010) : 305-318.
http://dx.doi.org/10.1016/j.jal.2010.08.010
---------- MLA ----------
Areces, C., Gorín, D. "Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction)" . Journal of Applied Logic, vol. 8, no. 4, 2010, pp. 305-318.
http://dx.doi.org/10.1016/j.jal.2010.08.010
---------- VANCOUVER ----------
Areces, C., Gorín, D. Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction). J. Appl. Logic. 2010;8(4):305-318.
http://dx.doi.org/10.1016/j.jal.2010.08.010