@inproceedings{Woelfl06,
  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.},
  added-at = {2016-08-05T15:59:03.000+0200},
  author = {W{\"o}lfl, Stefan and Mossakowski, Till and Schr{\"o}der, Lutz},
  biburl = {https://www.bibsonomy.org/bibtex/21f2062baeaaebbd8d9c108b1c4eca1dd/tillmo},
  booktitle = {20th International FLAIRS Conference (FLAIRS-20)},
  editor = {Wilson, David and Sutcliffe, Geoff},
  interhash = {0ce53ddceda86e01faaf719003cdcf72},
  intrahash = {1f2062baeaaebbd8d9c108b1c4eca1dd},
  keywords = {calculus composition heterogeneous qualitative table verification},
  pages = {665-670},
  pdfurl = {http://www.informatik.uni-bremen.de/~till/papers/qcc-comp-final.pdf},
  publisher = {AAAI Press},
  status = {Reviewed},
  timestamp = {2016-08-05T15:59:03.000+0200},
  title = { Qualitative Constraint Calculi: Heterogeneous Verification of Composition Tables},
  year = 2007
}