Tableau-based decision procedures for the logics of subinterval structures over dense orderings
Journal of Logic and Computation(2008)
摘要
In this paper, we develop tableau-based decision procedures for the logics of subinterval structures over dense linear orderings. In particular, we consider the two dicult cases: the relation of strict subin- tervals (with both endpoints strictly inside the current interval) and the relation of proper subintervals (that can share one endpoint with the cur- rent interval). For each of these logics, we establish a small pseudo-model property and construct a sound, complete, and terminating tableau that searches systematically for existence of such a pseudo-model satisfying the input formulas. Both constructions are non-trivial, but the latter is substantially more complicated because of the presence of beginning and ending subintervals which require special treatment. We prove PSPACE completeness for both procedures and implement them in the generic tableau-based theorem prover Lotrec.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络