Depth-First Reasoning on Trees

Authors

  • 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

Keywords:

Calculus, automated reasoning, depth-first search, XPath

Abstract

The mu-calculus is an expressive modal logic with least and greatest fixed-point operators. This formalism encompasses many temporal, program and description logics, and it has been widely applied in a broad 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 converse modalities 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 mu-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.

Author Biographies

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.

Downloads

Published

2018-03-30

Issue

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

Section

Articles of the Thematic Issue

License 

Hereby I transfer exclusively to the Journal "Computación y 
Sistemas", published by the Computing Research Center (CIC-IPN),
the Copyright of the aforementioned paper. I also accept that these 
rights will not be transferred to any other publication, in any other 
format, language or other existing means of developing.
I certify that the paper has not been previously disclosed or simultaneo
usly submitted to any other publication, and that it does not contain 
material whose publication would violate the Copyright or other 
proprietary rights of any person, company or institution. I certify that 
I have the permission from the institution or company where I work or 
study to publish this work.
The representative author accepts the responsibility for the publication
of this paper on behalf of each and every one of the authors. 
This transfer is subject to the following conditions:
  • The authors retain all ownership rights (such as patent rights) of this work, except for the publishing rights transferred to the CIC, through this document.
  • Authors retain the right to publish the work in whole or in part in any book they are the authors or publishers. They can also make use of this work in conferences, courses, personal web pages, and so on.
  • Authors may include working as part of his thesis, for non-profit distribution only.