具有分级路径和名义项的树逻辑
计算机科学中的逻辑
2010-06-02 v1
摘要
正则树文法和正则路径表达式是编程语言和类型系统中广泛使用的核心构造。然而，迄今为止，关于路径表达式（其中节点基数约束出现在树中的路径上）的推理框架研究甚少。我们提出了一种逻辑，能够表达沿路径的深度计数，该路径可以包含任意递归的前向和后向导航。这种计数扩展可以看作是对直接后继节点进行计数的分级模态的推广。虽然分级模态、名义项和逆模态的组合在图结构上会导致不可判定的逻辑，但我们证明，这些特性可以在树逻辑中结合，并在指数时间内可判定。
引用
@article{arxiv.1005.5623,
title = {A Tree Logic with Graded Paths and Nominals},
author = {Everardo Barcenas and Pierre Geneves and Nabil Layaida and Alan Schmitt},
journal= {arXiv preprint arXiv:1005.5623},
year = {2010}
}