Tableaux for Logics of Subinterval Structures over Dense Orderings

DAVIDE BRESOLIN, Department of Computer Science, University of Verona,
Verona, Italy
E-mail: bresolin@sci.univr.it
VALENTIN GORANKO, School of Mathematics, University of the
Witwatersrand, Johannesburg, South Africa
E-mail: goranko@maths.wits.ac.za
ANGELO MONTANARI and PIETRO SALA, Department of Mathematics and
Computer Science, University of Udine, Udine, Italy
E-mail: angelo.montanari@dimi.uniud.it; pietro.sala@dimi.uniud.it

Abstract
In this article, we develop tableau-based decision procedures for the logics of subinterval structures over dense linear orderings. In particular, we consider the two difficult cases: the relation of strict subintervals (with both endpoints strictly inside the current interval) and the relation of proper subintervals (that can share one endpoint with the current 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.

1 Introduction
Interval-based temporal logics provide a natural framework for temporal representation and
reasoning. Unfortunately, in the interval temporal logic setting undecidability is the rule (see, for
instance [16, 17]). The quest for decidable fragments and systems of temporal logics with intervalbased
semantics is one of the main research problems in the area of interval logics. Several
decidability results have been established previously by reduction to point-based logics, either
by selection of an appropriate subset of temporal operators or by restriction of the semantics,
e.g. imposing locality, homogeneity or other principles that essentially reduce it to point-based
semantics [1–3, 12–14, 18, 22]. Only recently some decidability results for genuinely interval-based
logics have been established [4–10].

(...)

In this article, we develop a sound, complete and terminating tableau system for D(symbol) .
(...)

The decision problem for D(symbol) is in PSPACE.
(...)
5 Implementation
In this section we briefly describe an implementation of the proposed tableau methods in Lotrec,
a generic theorem prover for modal and description logics [11, 15].
(...)
5.1 A short overview of Lotrec
Lotrec is a generic prover that can be used for most modal logics studied in the literature. It can be
used to prove validity and satisfiability of formulas. Whenever a formula is satisfiable, it returns a
model for it; whenever a formula is not valid, it returns a counter model for it. In Lotrec, a tableau is
a special kind of labelled graph that is built, and possibly revised, according to a set of user-specified
rules. Every node of the graph is labelled with a set of formulae and can be enriched by auxiliary
markings, if needed.
(...)
6 Conclusions
In this article, we investigated the decidability problem for logics of subinterval structures over
dense linear orderings. First, we systematically studied the logic D
· of the strict subinterval relation.
We provided an alternative proof of its decidability by a non-standard small-model theorem and
we developed an optimal tableau-based decision procedure for it. Then, we showed how to refine
structures and techniques for D
· to cope with the logic D
of the proper subinterval relation. We
proved that it is decidable as well, and we devise an optimal tableau-based decision procedure for
it. Finally, we implemented both tableau methods in Lotrec, a generic theorem prover for modal and
description logics.

http://logcom.oxfordjournals.org/cgi/reprint/exn063