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 breadth- first search for proofs.
Original language | English |
---|---|
Title of host publication | 10th International Conference on Distributed Multimedia Systems, International Workshop on Visual Languages and Computing |
Place of Publication | Skokie, IL, USA |
Publisher | Knowledge Systems Institute |
Pages | 91-98 |
Number of pages | 8 |
Publication status | Published - 1 Jan 2004 |
Event | 10th International Conference on Distributed Multimedia Systems, International Workshop on Visual Languages and Computing - Oak Brook, Illinois, USA Duration: 1 Jan 2004 → … |
Workshop
Workshop | 10th International Conference on Distributed Multimedia Systems, International Workshop on Visual Languages and Computing |
---|---|
Period | 1/01/04 → … |