Sciweavers

Share
TABLEAUX
1999
Springer

Merge Path Improvements for Minimal Model Hyper Tableaux

11 years 5 months ago
Merge Path Improvements for Minimal Model Hyper Tableaux
We combine techniques originally developed for refutational first-order theorem proving within the clause tree framework with techniques for minimal model computation developed within the hyper tableau framework. This combination generalizes well-known tableaux techniques like complement splitting and folding-up/down. We argue that this combination allows for efficiency improvements over previous, related methods. It is motivated by application to diagnosis tasks; in particular the problem of avoiding redundancies in the diagnoses of electrical circuits with reconvergent fanouts is addressed by the new technique. In the paper we develop as our main contribution in a more general way a sound and complete calculus for propositional circumscriptive reasoning in the presence of minimized and varying predicates.
Peter Baumgartner, Joseph Douglas Horton, Bruce Sp
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1999
Where TABLEAUX
Authors Peter Baumgartner, Joseph Douglas Horton, Bruce Spencer
Comments (0)
books