Qualitative räumliche Kalküle dienen der Repräsentation von
qualitativem Wissen über räumliche Verhältnisse, etwa in Kategorien
wie links, rechts, auf, unter, innerhalb, und der Schlußfolgerung aus
solchem Wissen. Die Folgerungsmethode basiert hierbei typischerweise
auf Tabellierungen möglicher Ergebnisse der Kombination räumlicher
Relationen; diese Tabellen sind allein schon wegen ihres Umfangs in
hohem Maße fehleranfällig. Wir demonstrieren die Verifikation der
Kompositionstabelle des RCC8-Kalküls (befasst mit Verhältnissen unter
räumlichen Regionen wie etwa Überlappung, Berührung etc.) im Bremer
heterogenen Werkzeug Hets. Dieses Werkzeug erlaubt die Kombination
verschiedener Verifikationslogiken und der dazugehörigen
logikspezifischen Werkzeuge, insbesondere automatischer und
halbautomatischer Beweiser. In der vorliegenden Verifikation werden
vollautomatische Beweise in Logik erster Stufe mit halbautomatischen
Beweisen in Logik höherer Stufe kombiniert.