Eugene Charniak, Saadia Husain
Finding best explanations is often formalized in AI in terms of minimal-cost proofs. Finding such proofs is naturally characterized as a best-first search of the proof-tree (actually a proof dag). Unfortunately the only known search heuristic for this task is quite poor. In this paper we present a new heuristic, a proof that it is admissible (for certain successor functions), and some experimental results suggesting that it is a significant improvement over the currently used heuristic.