Tech Report CS-91-11
A New Admissible Heuristic for Minimal-Cost Proofs
Eugene Charniak and 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.
(complete text in pdf)