Merge path improvements for minimal model hyper tableaux

5Citations
Citations of this article
2Readers
Mendeley users who have this article in their library.

You may have access to this PDF.

Abstract

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.

Cite

CITATION STYLE

APA

Baumgartner, P., Horton, J. D., & Spencer, B. (1999). Merge path improvements for minimal model hyper tableaux. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1617, pp. 51–66). Springer Verlag. https://doi.org/10.1007/3-540-48754-9_9

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free