Reference:
Ioerger, T. (1997). Integrating a spatial reasoner with a resolution theorem-prover. Fourteenth National Conference on Artificial Intelligence, 145-152.
Abstract:
Some spatial reasoning systems use images to solve problems, rather than
making formal logical inferences. However, an open question is how to use
these systems in contexts where some non-spatial information is also involved.
We present a hybrid reasoning method in which we extend the capabilities of a
spatial reasoner by integrating it with a resolution theorem-prover. We prove
that the hybrid system is refutation-complete, in the sense that, if a domain
theory is unsatisfiable, perhaps only because all of its models entail
unrealizable images, then our algorithm will halt. We discuss how our
approach differs from other hybrid reasoning algorithms in the way it manages
the interaction between sub-systems.