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

Keywords

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

Fingerprint Dive into the research topics of 'Automated theorem proving with spider diagrams'. Together they form a unique fingerprint.

Cite this