Depth-First Reasoning on Trees



Document title: Depth-First Reasoning on Trees
Journal: Computación y Sistemas
Database: PERIÓDICA
System number: 000423256
ISSN: 1405-5546
Authors: 1
2
2
3
Institutions: 1Universidad Veracruzana, Veracruz. México
2Consejo Nacional de Ciencia y Tecnología, Ciudad de México. México
3Universidad Politécnica de Puebla, Puebla. México
Year:
Season: Ene-Mar
Volumen: 22
Number: 1
Country: México
Language: Inglés
Document type: Artículo
Approach: Aplicado, descriptivo
English abstract The μ-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 μ-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 μ-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
Disciplines: Ciencias de la computación,
Matemáticas
Keyword: Procesamiento de datos,
Matemáticas aplicadas,
Cálculo,
Razonamiento automatizado,
Algoritmos
Keyword: Data processing,
Applied mathematics,
Calculus,
Automated reasoning,
Algorithms
Full text: Texto completo (Ver HTML) Texto completo (Ver PDF)