### Abstract

Original language | English |
---|---|

Pages (from-to) | 246-263 |

Number of pages | 18 |

Journal | Electronic Notes in Theoretical Computer Science |

Volume | 91 |

DOIs | |

Publication status | Published - 16 Feb 2004 |

### Fingerprint

### Keywords

- spider diagrams
- diagrammatic reasoning
- automated reasoning
- proof writing

### Cite this

*Electronic Notes in Theoretical Computer Science*,

*91*, 246-263. https://doi.org/10.1016/j.entcs.2003.12.016

}

*Electronic Notes in Theoretical Computer Science*, vol. 91, pp. 246-263. https://doi.org/10.1016/j.entcs.2003.12.016

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

Research output: Contribution to journal › Article

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 -