Generating proofs with spider diagrams using heuristics

Jean Flower; Judith Masthoff; Gem Stapleton

Generating proofs with spider diagrams using heuristics

Jean Flower
, Judith Masthoff
, Gem Stapleton

University of Brighton

Research output: Chapter in Book/Conference proceeding with ISSN or ISBN › Conference contribution with ISSN or ISBN › peer-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 language	English
Title of host publication	10th International Conference on Distributed Multimedia Systems, International Workshop on Visual Languages and Computing
Place of Publication	Skokie, IL, USA
Publisher	Knowledge Systems Institute
Pages	91-98
Number of pages	8
Publication status	Published - 1 Jan 2004
Event	10th International Conference on Distributed Multimedia Systems, International Workshop on Visual Languages and Computing - Oak Brook, Illinois, USA Duration: 1 Jan 2004 → …

Workshop

Workshop	10th International Conference on Distributed Multimedia Systems, International Workshop on Visual Languages and Computing
Period	1/01/04 → …

Access to Document

VLc04.pdfSubmitted manuscript, 153 KBLicence: Unspecified

http://homepages.abdn.ac.uk/j.masthoff/pages/Publications/VLC04.pdfLicence: Unspecified

Cite this

@inproceedings{ced922e3517144df9b325501c121b8a7,

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.",

author = "Jean Flower and Judith Masthoff and Gem Stapleton",

year = "2004",

month = jan,

day = "1",

language = "English",

pages = "91--98",

booktitle = "10th International Conference on Distributed Multimedia Systems, International Workshop on Visual Languages and Computing",

publisher = "Knowledge Systems Institute",

note = "10th International Conference on Distributed Multimedia Systems, International Workshop on Visual Languages and Computing ; Conference date: 01-01-2004",

}

Flower, J, Masthoff, J & Stapleton, G 2004, Generating proofs with spider diagrams using heuristics. in 10th International Conference on Distributed Multimedia Systems, International Workshop on Visual Languages and Computing. Knowledge Systems Institute, Skokie, IL, USA, pp. 91-98, 10th International Conference on Distributed Multimedia Systems, International Workshop on Visual Languages and Computing, 1/01/04. <http://homepages.abdn.ac.uk/j.masthoff/pages/Publications/VLC04.pdf>

Generating proofs with spider diagrams using heuristics. / Flower, Jean; Masthoff, Judith; Stapleton, Gem.
10th International Conference on Distributed Multimedia Systems, International Workshop on Visual Languages and Computing. Skokie, IL, USA: Knowledge Systems Institute, 2004. p. 91-98.

Research output: Chapter in Book/Conference proceeding with ISSN or ISBN › Conference contribution with ISSN or ISBN › peer-review

TY - GEN

T1 - Generating proofs with spider diagrams using heuristics

AU - Flower, Jean

AU - Masthoff, Judith

AU - Stapleton, Gem

PY - 2004/1/1

Y1 - 2004/1/1

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.

M3 - Conference contribution with ISSN or ISBN

SP - 91

EP - 98

BT - 10th International Conference on Distributed Multimedia Systems, International Workshop on Visual Languages and Computing

PB - Knowledge Systems Institute

CY - Skokie, IL, USA

T2 - 10th International Conference on Distributed Multimedia Systems, International Workshop on Visual Languages and Computing

Y2 - 1 January 2004

ER -

Generating proofs with spider diagrams using heuristics

Abstract

Workshop

Access to Document

Fingerprint

Cite this