Depth-First Reasoning on Trees

Autores/as

  • Yensen Limon Priego Universidad Veracruzana
  • Everardo Ismael Bárcenas Patiño CONACYT
  • Edgard Iván Benıtez Guerrero CONACYT
  • Maria Auxilio Medina Nieto Universidad Politécnica de Puebla

DOI:

https://doi.org/10.13053/cys-22-1-2776

Palabras clave:

Calculus, automated reasoning, depth-first search, XPath

Resumen

The mu-calculus is an expressive modallogic with least and greatest fixed-point operators. This formalism encompasses many temporal, program and description logics, and it has been widely applied in abroad range of domains, such as, program verification, knowledge representation and concurrent pervasive systems. In this paper, we propose a satisfiability algorithm for the mu-calculus extended with conversemodalities and interpreted on unranked trees. In contrast with known satisfiability algorithms, our proposal is based on a depth-first search. We prove the algorithm to be correct (sound and complete) and optimal. We also describe an implementation. The extension of the -calculus with converse modalities allows to efficiently characterize standard reasoning problems (emptiness, containment and equivalence) of XPath queries. We also describe several query reasoning experiments, which shows our proposal to be competitive in practice with known implementations.

Biografía del autor/a

Yensen Limon Priego, Universidad Veracruzana

Yensen Limón is a Ph.D. student at the Statistics and Computer Sciences Department in the University of Veracruz, Mexico. His research interests include Automated Reasoning, Modal Logics, and Context-Aware Computing.

Everardo Ismael Bárcenas Patiño, CONACYT

Everardo Bárcenas is a researcher at the National Council of Science and Technology (CONACYT), Mexico. He obtained a Ph.D. from the University of Grenoble, France. His research interests include Automated Reasoning, Modal Logics, Knowledge Representation, and Formal Methods.

Edgard Iván Benıtez Guerrero, CONACYT

Edgard Benítez Guerrero is a Professor at the Statistics and Computer Sciences Department in the University of Veracruz, Mexico. He obtained a Ph.D. from the University of Grenoble, France. His research interests include Context-Aware Computing, Databases and Artificial Intelligence.

Maria Auxilio Medina Nieto, Universidad Politécnica de Puebla

Ma. Auxilio Medina is the Coordinator of the Masters in Management and Technological Innovation in the Polytechnic University of Puebla, Mexico. She obtained a Ph.D. from the University of the Americas, Mexico. Her research interests include Semantic Web, Knowledge Representation and Information and Communications Technologies.

Descargas

Publicado

2018-03-30

Número

Vol. 22 Núm. 1 (2018): Thematic Issue on Language & Knowledge Engineering (Guest Editors: D. Pinto, D. Vilariño, B. Beltrán)

Sección

Articles of the Thematic Issue

Licencia

Transfiero exclusivamente a la revista “Computación y Sistemas”, editada por el Centro de Investigación en Computación (CIC), los Derechos de Autor del artículo antes mencionado, asimismo acepto que no serán transferidos a ninguna otra publicación, en cualquier formato, idioma, medio existente (incluyendo los electrónicos y multimedios) o por desarrollar.

Certifico que el artículo, no ha sido divulgado previamente o sometido simultáneamente a otra publicación y que no contiene materiales cuya publicación violaría los Derechos de Autor u otros derechos de propiedad de cualquier persona, empresa o institución. Certifico además que tengo autorización de la institución o empresa donde trabajo o estudio para publicar este Trabajo.

El autor, representante acepta la responsabilidad por la publicación del Trabajo en nombre de todos y cada uno de los autores.

Esta Transferencia está sujeta a las siguientes reservas:

  • Los autores conservan todos los derechos de propiedad (tales como derechos de patente) de este Trabajo, con excepción de los derechos de publicación transferidos al CIC, mediante este documento.
  • Los autores conservan el derecho de publicar el Trabajo total o parcialmente en cualquier libro del que ellos sean autores o editores y hacer uso personal de este trabajo en conferencias, cursos, páginas web personal, etc.