Generating proofs with spider diagrams using heuristics

Jean Flower, Judith Masthoff, Gemma Stapleton

Research output: Chapter in Book/Report/Conference proceedingPublished conference contribution


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 publicationProceedings of 10th international conference on distributed multimedia systems
Subtitle of host publicationInternational workshop on visual languages and computing, Knowledge Systems Institute
Number of pages8
Publication statusPublished - 2004
EventThe Tenth International Conference on Distributed Multimedia Systems, DMS'2004 - San Francisco, United States
Duration: 8 Sep 200410 Sep 2004


ConferenceThe Tenth International Conference on Distributed Multimedia Systems, DMS'2004
Country/TerritoryUnited States
CitySan Francisco


  • diagrammatic reasoning, spider diagrams, theorem provers, heuristics


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

Cite this