Generating proofs with spider diagrams using heuristics

Jean Flower, Judith Masthoff, Gemma Stapleton

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 publicationProceedings of 10th international conference on distributed multimedia systems
Subtitle of host publicationInternational workshop on visual languages and computing, Knowledge Systems Institute
Pages91-98
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

Conference

ConferenceThe Tenth International Conference on Distributed Multimedia Systems, DMS'2004
CountryUnited States
CitySan Francisco
Period8/09/0410/09/04

Keywords

  • diagrammatic reasoning, spider diagrams, theorem provers, heuristics

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

  • Cite this

    Flower, J., Masthoff, J., & Stapleton, G. (2004). Generating proofs with spider diagrams using heuristics. In Proceedings of 10th international conference on distributed multimedia systems: International workshop on visual languages and computing, Knowledge Systems Institute (pp. 91-98) http://eprints.brighton.ac.uk/2849/