Generating proofs with spider diagrams using heuristics

Jean Flower; Judith Masthoff; Gemma Stapleton

Generating proofs with spider diagrams using heuristics

Jean Flower, Judith Masthoff, Gemma Stapleton

Computing Science

Research output: Chapter in Book/Report/Conference proceeding › Published conference 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 language	English
Title of host publication	Proceedings of 10th international conference on distributed multimedia systems
Subtitle of host publication	International workshop on visual languages and computing, Knowledge Systems Institute
Pages	91-98
Number of pages	8
Publication status	Published - 2004
Event	The Tenth International Conference on Distributed Multimedia Systems, DMS'2004 - San Francisco, United States Duration: 8 Sept 2004 → 10 Sept 2004

Conference

Conference	The Tenth International Conference on Distributed Multimedia Systems, DMS'2004
Country/Territory	United States
City	San Francisco
Period	8/09/04 → 10/09/04

Bibliographical note

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

Keywords

diagrammatic reasoning, spider diagrams, theorem provers, heuristics

Access to Document

http://eprints.brighton.ac.uk/2849/

Cite this

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 proceeding › Published conference 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. <http://eprints.brighton.ac.uk/2849/>

@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; The Tenth International Conference on Distributed Multimedia Systems, DMS'2004 ; Conference date: 08-09-2004 Through 10-09-2004",

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 - Published conference contribution

SP - 91

EP - 98

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

T2 - The Tenth International Conference on Distributed Multimedia Systems, DMS'2004

Y2 - 8 September 2004 through 10 September 2004

ER -

Generating proofs with spider diagrams using heuristics

Abstract

Conference

Bibliographical note

Keywords

Access to Document

Fingerprint

Cite this