Semantically Guided Theorem Proving for Diagnosis Applications.
Peter Baumgartner, Peter H. Fröhlich, Ulrich Furbach, Wolfgang Nejdl · 1997
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 diagnoses. Our experiments show that our general approach is competitive with specialized diagnosis systems.