Tableaux for Diagnosis Applications
Peter Baumgartner, Peter Fröhlich, Ulrich Furbach and
Wolfgang Nejdl
Abstract
With DRUM-2 a very efficient system for solving
diagnosis tasks has been described, which is based on belief
revision procedures and uses first order logic system descriptions.
In this paper we demonstrate how such a system can be rigorously
formalized from the viewpoint of deduction by using the calculus of
hyper tableaux. The
benefits of this approach are twofold: first, it gives us a clear
logical description of the diagnosis task to be solved; second, as
our experiments show, the approach is feasible in practice and thus
serves as an example of a successful application of deduction
techniques to real-world applications.
Keywords: Diagnosis, Automated Reasoning
The full report is available as a
postscript file .