Generating readable proofs: a heuristic approach to theorum proving with spider diagrams

Jean Flower, Judith Masthoff, Gem Stapleton

Research output: Chapter in Book/Conference proceeding with ISSN or ISBNConference contribution with ISSN or ISBN

Abstract

An important aim of diagrammatic reasoning is to make it easier for people to create and understand logical arguments. We have worked on spider diagrams, which visually express logical statements. Ideally, automatically generated proofs should be short and easy to understand. An existing proof generator for spider diagrams successfully writes proofs, but they can be long and unwieldy. In this paper, we present a new approach to proof writing in diagrammatic systems, which is guaranteed to find shortest proofs and can be extended to incorporate other readability criteria. We apply the A* algorithm and develop an admissible heuristic function to guide automatic proof construction. We demonstrate the effectiveness of the heuristic used. The work has been implemented as part of a spider diagram reasoning tool.
Original languageEnglish
Title of host publicationProceedings of the Third International Conference, Diagrams 2004
EditorsA. Blackwell, K. Marriott, A. Shimojima
Place of PublicationBerlin, Germany
PublisherSpringer-Verlag
Pages166-181
Number of pages16
Volume2980
ISBN (Print)9783540212683
DOIs
Publication statusPublished - 1 Jan 2004
EventProceedings of the Third International Conference, Diagrams 2004 - Cambridge, UK, March 22-24, 2004
Duration: 1 Jan 2004 → …

Publication series

NameLecture Notes in Computer Science

Conference

ConferenceProceedings of the Third International Conference, Diagrams 2004
Period1/01/04 → …

Keywords

  • Visual languages
  • Spider diagrams
  • Heuristics

Cite this

Flower, J., Masthoff, J., & Stapleton, G. (2004). Generating readable proofs: a heuristic approach to theorum proving with spider diagrams. In A. Blackwell, K. Marriott, & A. Shimojima (Eds.), Proceedings of the Third International Conference, Diagrams 2004 (Vol. 2980, pp. 166-181). (Lecture Notes in Computer Science). Berlin, Germany: Springer-Verlag. https://doi.org/10.1007/978-3-540-25931-2_17
Flower, Jean ; Masthoff, Judith ; Stapleton, Gem. / Generating readable proofs: a heuristic approach to theorum proving with spider diagrams. Proceedings of the Third International Conference, Diagrams 2004. editor / A. Blackwell ; K. Marriott ; A. Shimojima. Vol. 2980 Berlin, Germany : Springer-Verlag, 2004. pp. 166-181 (Lecture Notes in Computer Science).
@inproceedings{8de6c368984149f2b342486b0d2a8c3a,
title = "Generating readable proofs: a heuristic approach to theorum proving with spider diagrams",
abstract = "An important aim of diagrammatic reasoning is to make it easier for people to create and understand logical arguments. We have worked on spider diagrams, which visually express logical statements. Ideally, automatically generated proofs should be short and easy to understand. An existing proof generator for spider diagrams successfully writes proofs, but they can be long and unwieldy. In this paper, we present a new approach to proof writing in diagrammatic systems, which is guaranteed to find shortest proofs and can be extended to incorporate other readability criteria. We apply the A* algorithm and develop an admissible heuristic function to guide automatic proof construction. We demonstrate the effectiveness of the heuristic used. The work has been implemented as part of a spider diagram reasoning tool.",
keywords = "Visual languages, Spider diagrams, Heuristics",
author = "Jean Flower and Judith Masthoff and Gem Stapleton",
year = "2004",
month = "1",
day = "1",
doi = "10.1007/978-3-540-25931-2_17",
language = "English",
isbn = "9783540212683",
volume = "2980",
series = "Lecture Notes in Computer Science",
publisher = "Springer-Verlag",
pages = "166--181",
editor = "A. Blackwell and K. Marriott and A. Shimojima",
booktitle = "Proceedings of the Third International Conference, Diagrams 2004",

}

Flower, J, Masthoff, J & Stapleton, G 2004, Generating readable proofs: a heuristic approach to theorum proving with spider diagrams. in A Blackwell, K Marriott & A Shimojima (eds), Proceedings of the Third International Conference, Diagrams 2004. vol. 2980, Lecture Notes in Computer Science, Springer-Verlag, Berlin, Germany, pp. 166-181, Proceedings of the Third International Conference, Diagrams 2004, 1/01/04. https://doi.org/10.1007/978-3-540-25931-2_17

Generating readable proofs: a heuristic approach to theorum proving with spider diagrams. / Flower, Jean; Masthoff, Judith; Stapleton, Gem.

Proceedings of the Third International Conference, Diagrams 2004. ed. / A. Blackwell; K. Marriott; A. Shimojima. Vol. 2980 Berlin, Germany : Springer-Verlag, 2004. p. 166-181 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Conference proceeding with ISSN or ISBNConference contribution with ISSN or ISBN

TY - GEN

T1 - Generating readable proofs: a heuristic approach to theorum proving with spider diagrams

AU - Flower, Jean

AU - Masthoff, Judith

AU - Stapleton, Gem

PY - 2004/1/1

Y1 - 2004/1/1

N2 - An important aim of diagrammatic reasoning is to make it easier for people to create and understand logical arguments. We have worked on spider diagrams, which visually express logical statements. Ideally, automatically generated proofs should be short and easy to understand. An existing proof generator for spider diagrams successfully writes proofs, but they can be long and unwieldy. In this paper, we present a new approach to proof writing in diagrammatic systems, which is guaranteed to find shortest proofs and can be extended to incorporate other readability criteria. We apply the A* algorithm and develop an admissible heuristic function to guide automatic proof construction. We demonstrate the effectiveness of the heuristic used. The work has been implemented as part of a spider diagram reasoning tool.

AB - An important aim of diagrammatic reasoning is to make it easier for people to create and understand logical arguments. We have worked on spider diagrams, which visually express logical statements. Ideally, automatically generated proofs should be short and easy to understand. An existing proof generator for spider diagrams successfully writes proofs, but they can be long and unwieldy. In this paper, we present a new approach to proof writing in diagrammatic systems, which is guaranteed to find shortest proofs and can be extended to incorporate other readability criteria. We apply the A* algorithm and develop an admissible heuristic function to guide automatic proof construction. We demonstrate the effectiveness of the heuristic used. The work has been implemented as part of a spider diagram reasoning tool.

KW - Visual languages

KW - Spider diagrams

KW - Heuristics

U2 - 10.1007/978-3-540-25931-2_17

DO - 10.1007/978-3-540-25931-2_17

M3 - Conference contribution with ISSN or ISBN

SN - 9783540212683

VL - 2980

T3 - Lecture Notes in Computer Science

SP - 166

EP - 181

BT - Proceedings of the Third International Conference, Diagrams 2004

A2 - Blackwell, A.

A2 - Marriott, K.

A2 - Shimojima, A.

PB - Springer-Verlag

CY - Berlin, Germany

ER -

Flower J, Masthoff J, Stapleton G. Generating readable proofs: a heuristic approach to theorum proving with spider diagrams. In Blackwell A, Marriott K, Shimojima A, editors, Proceedings of the Third International Conference, Diagrams 2004. Vol. 2980. Berlin, Germany: Springer-Verlag. 2004. p. 166-181. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-540-25931-2_17