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

Fingerprint

Theorem proving
Acoustic waves

Keywords

  • diagrammatic reasoning, spider diagrams, theorem provers, heuristics

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)

Generating proofs with spider diagrams using heuristics. / Flower, Jean; Masthoff, Judith; Stapleton, Gemma.

Proceedings of 10th international conference on distributed multimedia systems: International workshop on visual languages and computing, Knowledge Systems Institute . 2004. p. 91-98.

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

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, The Tenth International Conference on Distributed Multimedia Systems, DMS'2004, San Francisco, United States, 8/09/04.
Flower J, Masthoff J, Stapleton G. 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 . 2004. p. 91-98
Flower, Jean ; Masthoff, Judith ; Stapleton, Gemma. / Generating proofs with spider diagrams using heuristics. Proceedings of 10th international conference on distributed multimedia systems: International workshop on visual languages and computing, Knowledge Systems Institute . 2004. pp. 91-98
@inproceedings{6d68c831c3de48389d03bd67f026931e,
title = "Generating proofs with spider diagrams using heuristics",
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.",
keywords = "diagrammatic reasoning, spider diagrams, theorem provers, heuristics",
author = "Jean Flower and Judith Masthoff and Gemma Stapleton",
note = "The Tenth International Conference on Distributed Multimedia Systems, DMS'2004, Organized by Knowledge Systems Institute, September 8 - 10, 2004, San Francisco Bay, CA",
year = "2004",
language = "English",
pages = "91--98",
booktitle = "Proceedings of 10th international conference on distributed multimedia systems",

}

TY - GEN

T1 - Generating proofs with spider diagrams using heuristics

AU - Flower, Jean

AU - Masthoff, Judith

AU - Stapleton, Gemma

N1 - The Tenth International Conference on Distributed Multimedia Systems, DMS'2004, Organized by Knowledge Systems Institute, September 8 - 10, 2004, San Francisco Bay, CA

PY - 2004

Y1 - 2004

N2 - 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.

AB - 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.

KW - diagrammatic reasoning, spider diagrams, theorem provers, heuristics

M3 - Conference contribution

SP - 91

EP - 98

BT - Proceedings of 10th international conference on distributed multimedia systems

ER -