A tractable class of abduction problems
Kave Eshghi · International Joint Conference on Artificial Intelligence · 1993
The problem of finding a set of assumptions which explain a given proposition is in general NP-hard, even when the background theory is an acyclic Horn theory. In this paper it is shown that when the background theory is acyclic Horn and its pseudo-completion is unit refutable, there is a polynomial time algorithm for finding minimal explanations. A test for unit-refutability of clausal theories is presented, based on the topology of the connection graph of the theory.