License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.05491.9
URN: urn:nbn:de:0030-drops-9798
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2007/979/
Go to the corresponding Portal

Wölfl, Stefan ; Mossakowski, Till ; Schröder, Lutz

Qualitative Constraint Calculi: Heterogeneous Verification of Composition Tables

pdf-format:
05491.WoelflStefan.Paper.979.pdf (0.2 MB)

Abstract

In the domain of qualitative constraint reasoning, a subfield of AI which has evolved in the past 25 years, a large number of calculi for efficient reasoning about spatial and temporal entities has been developed. Reasoning techniques developed for these constraint calculi typically rely on so-called composition tables of the calculus at hand, which allow for replacing semantic reasoning by symbolic operations. Often these composition tables are developed in a quite informal, pictorial manner and hence composition tables are prone to errors. In view of possible safety critical applications of
qualitative calculi, however, it is desirable to formally verify these composition tables. In general, the verification of composition tables is a tedious task, in particular in cases where the semantics of the calculus depends on higher-order constructs such as sets. In this paper we address this problem by presenting a heterogeneous proof method that allows for combining a higher-order proof assistance system (such as Isabelle) with an automatic (first order) reasoner (such as SPASS or VAMPIRE). The benefit of this method is that the number of proof obligations that is to be proven interactively with a semi-automatic reasoner can be minimized to an acceptable level.

BibTeX - Entry

@InProceedings{wolfl_et_al:DagSemProc.05491.9,
  author =	{W\"{o}lfl, Stefan and Mossakowski, Till and Schr\"{o}der, Lutz},
  title =	{{Qualitative Constraint Calculi: Heterogeneous Verification of Composition Tables}},
  booktitle =	{Spatial Cognition: Specialization and Integration},
  pages =	{1--12},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{5491},
  editor =	{Anthony G. Cohn and Christian Freksa and Bernhard Nebel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2007/979},
  URN =		{urn:nbn:de:0030-drops-9798},
  doi =		{10.4230/DagSemProc.05491.9},
  annote =	{Keywords: Knowledge representation and reasoning, geometric and spatial reasoning, qualitative reasoning, automated versus interaction proving, heterogeneous}
}

Keywords: Knowledge representation and reasoning, geometric and spatial reasoning, qualitative reasoning, automated versus interaction proving, heterogeneous
Collection: 05491 - Spatial Cognition: Specialization and Integration
Issue Date: 2007
Date of publication: 25.04.2007

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI