Integrating a spatial reasoner with a resolution theorem-prover Conference Paper uri icon


  • 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.

published proceedings

  • Proceedings of the National Conference on Artificial Intelligence

author list (cited authors)

  • Ioerger, T. R.

complete list of authors

  • Ioerger, TR

editor list (cited editors)

  • Kuipers, B., & Webber, B. L.

publication date

  • December 1997