by Stefan Wölfl, Till Mossakowski and Lutz Schröder
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 have been developed. Reasoning techniques developed for these constraint calculi typically rely on the respective composition table of the calculus at hand, but often these composition tables are developed in a quite informal manner only and hence are prone to errors. In view of possible safety critical applications of qualitative calculi it is desirable to formally verify these composition tables. In general, however, the verification of composition tables is a tedious task, in particular, in those 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). The benefit of this method is that the number of proof obligations that is to be proven by hand with a semi-automatic reasoner can be minimized to an acceptable level.
Reference:
Stefan Wölfl, Till Mossakowski and Lutz Schröder: Qualitative Constraint Calculi: Heterogeneous Verification of Composition Tables, In David Wilson, Geoff Sutcliffe, eds.: 20th International FLAIRS Conference (FLAIRS-20), pp. 665–670, AAAI Press, 2007. [preprint]
Bibtex Entry:
@InProceedings{Woelfl06,
author = {Stefan W{\"o}lfl and Till Mossakowski and Lutz Schr{\"o}der},
title = { Qualitative Constraint Calculi: Heterogeneous Verification of Composition Tables},
year = {2007},
editor = {David Wilson and Geoff Sutcliffe},
booktitle = {20th International FLAIRS Conference (FLAIRS-20)},
publisher = {AAAI Press},
pages = {665-670},
keywords = {composition table qualitative calculus verification heterogeneous},
comment = { <a href = "http://www.informatik.uni-bremen.de/~till/papers/qcc-comp-final.pdf"> [preprint] </a>},
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 have been
developed. Reasoning techniques developed for these constraint
calculi typically rely on the respective composition table of the
calculus at hand, but often these composition tables are developed
in a quite informal manner only and hence are prone to errors. In
view of possible safety critical applications of qualitative calculi
it is desirable to formally verify these composition tables. In
general, however, the verification of composition tables is a
tedious task, in particular, in those 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). The benefit of this method is that the number of
proof obligations that is to be proven by hand with a semi-automatic
reasoner can be minimized to an acceptable level.},
}