Generating proofs with spider diagrams using heuristics

Jean Flower, Judith Masthoff, Gem Stapleton

Research output: Chapter in Book/Conference proceeding with ISSN or ISBNConference contribution with ISSN or ISBNpeer-review

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 languageEnglish
Title of host publication10th International Conference on Distributed Multimedia Systems, International Workshop on Visual Languages and Computing
Place of PublicationSkokie, IL, USA
PublisherKnowledge Systems Institute
Pages91-98
Number of pages8
Publication statusPublished - 1 Jan 2004
Event10th International Conference on Distributed Multimedia Systems, International Workshop on Visual Languages and Computing - Oak Brook, Illinois, USA
Duration: 1 Jan 2004 → …

Workshop

Workshop10th International Conference on Distributed Multimedia Systems, International Workshop on Visual Languages and Computing
Period1/01/04 → …

Fingerprint

Dive into the research topics of 'Generating proofs with spider diagrams using heuristics'. Together they form a unique fingerprint.

Cite this