Abstract: |
Systems for qualitative spatial reasoning (QSR)
are usually formulated as relation algebras,
and reasoning in such systems is performed by
constraint-satisfaction techniques. While this
is often adequate, it is a rather inexpressive
framework that cannot model and solve many spatial
reasoning problems; it can also complicate the
combination of different spatial formalisms, e.g.,
the combination of topological with metric primitives,
or absolute orientation with relative orientation.
Here we suggest an alternative approach, whereby
spatial information is expressed in a rich quantified
3-valued logic, equipped with a novel semantics for
dealing with incomplete information. Decidability
is ensured by a systematic compilation into propositional
logic and the use of SAT solvers. To illustrate,
we define and implement a new system for two-dimensional
positional reasoning that combines Frank's cardinal-direction
calculus, the flip-flop calculus for reasoning about
relative orientation, and various new positional
primitives. Unlike previous work, the system uses
diagrams as well as symbolic formulas. In particular,
the logic we introduce is {\em heterogeneous}, meaning
that it combines symbolic and diagrammatic representation
and inference. |