Generating readable proofs: A heuristic approach to theorem proving with spider diagrams

J. Flower; Judith Francoise Maria Masthoff; G. Stapleton

doi:10.1007/978-3-540-25931-2_17

Generating readable proofs: A heuristic approach to theorem proving with spider diagrams

J. Flower, Judith Francoise Maria Masthoff, G. Stapleton

Computing Science

University of Brighton

Research output: Chapter in Book/Report/Conference proceeding › Published conference contribution

22 Citations (Scopus)

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 language	English
Title of host publication	Diagrammatic Representation and Inference
Subtitle of host publication	Third International Conference, Diagrams 2004, Cambridge, UK, March 22-24, 2004, Proceedings
Editors	Alan F. Blackwell, Kim Marriott, Atsushi Shimojima
Place of Publication	Berlin
Publisher	Springer
Pages	166-181
Number of pages	16
ISBN (Electronic)	978-3-540-25931-2
ISBN (Print)	978-3-540-21268-3
DOIs	https://doi.org/10.1007/978-3-540-25931-2_17
Publication status	Published - Mar 2004
Event	Third International Conference on the Theory and Application of Diagrams (Diagrams 2004) - Cambridge, United Kingdom Duration: 22 Mar 2004 → 24 Mar 2004

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	2980
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	Third International Conference on the Theory and Application of Diagrams (Diagrams 2004)
Country/Territory	United Kingdom
City	Cambridge
Period	22/03/04 → 24/03/04

Bibliographical note

Gem Stapleton thanks the UK EPSRC for support under grant number 01800274.
Jean Flower was partially supported by the UK EPSRC grant GR/R63516.

Access to Document

10.1007/978-3-540-25931-2_17Licence: Unspecified

Cite this

Flower, J., Masthoff, J. F. M., & Stapleton, G. (2004). Generating readable proofs: A heuristic approach to theorem proving with spider diagrams. In A. F. Blackwell, K. Marriott, & A. Shimojima (Eds.), Diagrammatic Representation and Inference : Third International Conference, Diagrams 2004, Cambridge, UK, March 22-24, 2004, Proceedings (pp. 166-181). (Lecture Notes in Computer Science; Vol. 2980). Springer . https://doi.org/10.1007/978-3-540-25931-2_17

Generating readable proofs: A heuristic approach to theorem proving with spider diagrams. / Flower, J.; Masthoff, Judith Francoise Maria; Stapleton, G.
Diagrammatic Representation and Inference : Third International Conference, Diagrams 2004, Cambridge, UK, March 22-24, 2004, Proceedings. ed. / Alan F. Blackwell; Kim Marriott; Atsushi Shimojima. Berlin: Springer , 2004. p. 166-181 (Lecture Notes in Computer Science; Vol. 2980).

Research output: Chapter in Book/Report/Conference proceeding › Published conference contribution

Flower, J, Masthoff, JFM & Stapleton, G 2004, Generating readable proofs: A heuristic approach to theorem proving with spider diagrams. in AF Blackwell, K Marriott & A Shimojima (eds), Diagrammatic Representation and Inference : Third International Conference, Diagrams 2004, Cambridge, UK, March 22-24, 2004, Proceedings. Lecture Notes in Computer Science, vol. 2980, Springer , Berlin, pp. 166-181, Third International Conference on the Theory and Application of Diagrams (Diagrams 2004) , Cambridge, United Kingdom, 22/03/04. https://doi.org/10.1007/978-3-540-25931-2_17

Flower J, Masthoff JFM, Stapleton G. Generating readable proofs: A heuristic approach to theorem proving with spider diagrams. In Blackwell AF, Marriott K, Shimojima A, editors, Diagrammatic Representation and Inference : Third International Conference, Diagrams 2004, Cambridge, UK, March 22-24, 2004, Proceedings. Berlin: Springer . 2004. p. 166-181. (Lecture Notes in Computer Science). doi: 10.1007/978-3-540-25931-2_17

Flower, J. ; Masthoff, Judith Francoise Maria ; Stapleton, G. / Generating readable proofs : A heuristic approach to theorem proving with spider diagrams. Diagrammatic Representation and Inference : Third International Conference, Diagrams 2004, Cambridge, UK, March 22-24, 2004, Proceedings. editor / Alan F. Blackwell ; Kim Marriott ; Atsushi Shimojima. Berlin : Springer , 2004. pp. 166-181 (Lecture Notes in Computer Science).

@inproceedings{381d38ac0e9243cdabd8547e248d175f,

title = "Generating readable proofs: A heuristic approach to theorem 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 proofgenerator for spider diagrams successfullywrites proofs, but they can be long andunwieldy. In this paper, wepresent a new approach to proof writingin diagrammatic systems, whichis guaranteed to find shortest proofs andcan be extended to incorporateother readability criteria. We apply the A∗algorithm and develop anadmissible heuristic function to guideautomatic proof construction. Wedemonstrate the effectiveness of theheuristic used. The work has beenimplemented as part of a spider diagramreasoning tool.",

author = "J. Flower and Masthoff, {Judith Francoise Maria} and G. Stapleton",

note = "Gem Stapleton thanks the UK EPSRC for support under grant number 01800274. Jean Flower was partially supported by the UK EPSRC grant GR/R63516.; Third International Conference on the Theory and Application of Diagrams (Diagrams 2004) ; Conference date: 22-03-2004 Through 24-03-2004",

year = "2004",

month = mar,

doi = "10.1007/978-3-540-25931-2_17",

language = "English",

isbn = "978-3-540-21268-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer ",

pages = "166--181",

editor = "Blackwell, {Alan F.} and Kim Marriott and Atsushi Shimojima",

booktitle = "Diagrammatic Representation and Inference",

}

TY - GEN

T1 - Generating readable proofs

T2 - Third International Conference on the Theory and Application of Diagrams (Diagrams 2004)

AU - Flower, J.

AU - Masthoff, Judith Francoise Maria

AU - Stapleton, G.

N1 - Gem Stapleton thanks the UK EPSRC for support under grant number 01800274. Jean Flower was partially supported by the UK EPSRC grant GR/R63516.

PY - 2004/3

Y1 - 2004/3

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 proofgenerator for spider diagrams successfullywrites proofs, but they can be long andunwieldy. In this paper, wepresent a new approach to proof writingin diagrammatic systems, whichis guaranteed to find shortest proofs andcan be extended to incorporateother readability criteria. We apply the A∗algorithm and develop anadmissible heuristic function to guideautomatic proof construction. Wedemonstrate the effectiveness of theheuristic used. The work has beenimplemented as part of a spider diagramreasoning 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 proofgenerator for spider diagrams successfullywrites proofs, but they can be long andunwieldy. In this paper, wepresent a new approach to proof writingin diagrammatic systems, whichis guaranteed to find shortest proofs andcan be extended to incorporateother readability criteria. We apply the A∗algorithm and develop anadmissible heuristic function to guideautomatic proof construction. Wedemonstrate the effectiveness of theheuristic used. The work has beenimplemented as part of a spider diagramreasoning tool.

UR - https://www.researchgate.net/publication/221249389_Generating_Readable_Proofs_A_Heuristic_Approach_to_Theorem_Proving_With_Spider_Diagrams

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

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

M3 - Published conference contribution

SN - 978-3-540-21268-3

T3 - Lecture Notes in Computer Science

SP - 166

EP - 181

BT - Diagrammatic Representation and Inference

A2 - Blackwell, Alan F.

A2 - Marriott, Kim

A2 - Shimojima, Atsushi

PB - Springer

CY - Berlin

Y2 - 22 March 2004 through 24 March 2004

ER -

Generating readable proofs: A heuristic approach to theorem proving with spider diagrams

Abstract

Publication series

Conference

Bibliographical note

Access to Document

Other files and links

Fingerprint

Cite this