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

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

Research output: Chapter in Book/Report/Conference proceedingPublished 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 languageEnglish
Title of host publicationDiagrammatic Representation and Inference
Subtitle of host publicationThird International Conference, Diagrams 2004, Cambridge, UK, March 22-24, 2004, Proceedings
EditorsAlan F. Blackwell, Kim Marriott, Atsushi Shimojima
Place of PublicationBerlin
PublisherSpringer
Pages166-181
Number of pages16
ISBN (Electronic)978-3-540-25931-2
ISBN (Print)978-3-540-21268-3
DOIs
Publication statusPublished - Mar 2004
EventThird International Conference on the Theory and Application of Diagrams (Diagrams 2004) - Cambridge, United Kingdom
Duration: 22 Mar 200424 Mar 2004

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume2980
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceThird International Conference on the Theory and Application of Diagrams (Diagrams 2004)
Country/TerritoryUnited Kingdom
CityCambridge
Period22/03/0424/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.

Fingerprint

Dive into the research topics of 'Generating readable proofs: A heuristic approach to theorem proving with spider diagrams'. Together they form a unique fingerprint.

Cite this