Generating proofs with spider diagrams using heuristics
Jean Flower, Judith Masthoff, Gem Stapleton · University of Brighton Repository (University of Brighton) · 2004
Abstract — We apply the A ∗ algorithm to guide a diagrammatic theorem proving tool. The algorithm requires a heuristic function, which provides a metric on the search space. In this paper we present a collection of metrics between two spider diagrams. We combine these metrics to give a heuristic function that provides a lower bound on the length of a shortest proof from one spider diagram to another, using a collection of sound reasoning rules. We compare the effectiveness of our approach with a breadthfirst search for proofs. I.