Semantically Guided Theorem Proving
for Diagnosis Applications
Peter Baumgartner, Peter Fröhlich, Ulrich Furbach
and Wolfgang Nejdl
Abstract
In this paper we demonstrate how general purpose automated theorem
proving techniques can be used to solve realistic model-based
diagnosis problems. For this we modify a model generating tableau
calculus such that a model of a correctly behaving device can be
used to guide the search for minimal n-fault diagnoses. Our
experiments show that our general approach is competitive with
specialized diagnosis systems.
Keywords: Diagnosis, Automated Reasoning
The full report is available as a
postscript file .