Automated theorem proving with spider diagrams

Jean Flower, Gem Stapleton

Research output: Contribution to journalArticle

Abstract

Spider diagrams are a visual notation for expressing logical statements. In this paper we describe a tool that supports reasoning with a sound and complete spider diagram system. The tool allows the construction of diagrams and proofs by users. We present an algorithm which the tool uses to determine whether one diagram semantically entails another. If the premise diagram does semantically entail the conclusion diagram then a proof is presented to the user. Otherwise it gives a counterexample: a model for the premise that is not a model for the conclusion. The proof of completeness given in [Howse, J., G. Stapleton and J. Taylor, Spider diagrams, In preparation, to appear: www.cmis.brighton.ac.uk/research/vmg] can be used to create an alternative proof writing algorithm. The algorithm described here improves upon this by providing counterexamples and significantly shorter proofs.
Original languageEnglish
Pages (from-to)246-263
Number of pages18
JournalElectronic Notes in Theoretical Computer Science
Volume91
DOIs
Publication statusPublished - 16 Feb 2004

Fingerprint

Automated Theorem Proving
Spiders
Diagram
Counterexample
Tool Support
Notation
Completeness
Preparation
Reasoning
Alternatives

Keywords

  • spider diagrams
  • diagrammatic reasoning
  • automated reasoning
  • proof writing

Cite this

Flower, Jean ; Stapleton, Gem. / Automated theorem proving with spider diagrams. In: Electronic Notes in Theoretical Computer Science. 2004 ; Vol. 91. pp. 246-263.
@article{785b304b8068401ab9186985917b14db,
title = "Automated theorem proving with spider diagrams",
abstract = "Spider diagrams are a visual notation for expressing logical statements. In this paper we describe a tool that supports reasoning with a sound and complete spider diagram system. The tool allows the construction of diagrams and proofs by users. We present an algorithm which the tool uses to determine whether one diagram semantically entails another. If the premise diagram does semantically entail the conclusion diagram then a proof is presented to the user. Otherwise it gives a counterexample: a model for the premise that is not a model for the conclusion. The proof of completeness given in [Howse, J., G. Stapleton and J. Taylor, Spider diagrams, In preparation, to appear: www.cmis.brighton.ac.uk/research/vmg] can be used to create an alternative proof writing algorithm. The algorithm described here improves upon this by providing counterexamples and significantly shorter proofs.",
keywords = "spider diagrams, diagrammatic reasoning, automated reasoning, proof writing",
author = "Jean Flower and Gem Stapleton",
year = "2004",
month = "2",
day = "16",
doi = "10.1016/j.entcs.2003.12.016",
language = "English",
volume = "91",
pages = "246--263",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",

}

Automated theorem proving with spider diagrams. / Flower, Jean; Stapleton, Gem.

In: Electronic Notes in Theoretical Computer Science, Vol. 91, 16.02.2004, p. 246-263.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Automated theorem proving with spider diagrams

AU - Flower, Jean

AU - Stapleton, Gem

PY - 2004/2/16

Y1 - 2004/2/16

N2 - Spider diagrams are a visual notation for expressing logical statements. In this paper we describe a tool that supports reasoning with a sound and complete spider diagram system. The tool allows the construction of diagrams and proofs by users. We present an algorithm which the tool uses to determine whether one diagram semantically entails another. If the premise diagram does semantically entail the conclusion diagram then a proof is presented to the user. Otherwise it gives a counterexample: a model for the premise that is not a model for the conclusion. The proof of completeness given in [Howse, J., G. Stapleton and J. Taylor, Spider diagrams, In preparation, to appear: www.cmis.brighton.ac.uk/research/vmg] can be used to create an alternative proof writing algorithm. The algorithm described here improves upon this by providing counterexamples and significantly shorter proofs.

AB - Spider diagrams are a visual notation for expressing logical statements. In this paper we describe a tool that supports reasoning with a sound and complete spider diagram system. The tool allows the construction of diagrams and proofs by users. We present an algorithm which the tool uses to determine whether one diagram semantically entails another. If the premise diagram does semantically entail the conclusion diagram then a proof is presented to the user. Otherwise it gives a counterexample: a model for the premise that is not a model for the conclusion. The proof of completeness given in [Howse, J., G. Stapleton and J. Taylor, Spider diagrams, In preparation, to appear: www.cmis.brighton.ac.uk/research/vmg] can be used to create an alternative proof writing algorithm. The algorithm described here improves upon this by providing counterexamples and significantly shorter proofs.

KW - spider diagrams

KW - diagrammatic reasoning

KW - automated reasoning

KW - proof writing

U2 - 10.1016/j.entcs.2003.12.016

DO - 10.1016/j.entcs.2003.12.016

M3 - Article

VL - 91

SP - 246

EP - 263

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -