Automated Theorem Proving in Euler Diagram Systems

Gem Stapleton, Judith Francoise Maria Masthoff, Jean Flower, Andrew Fish, Jane Southern

Research output: Contribution to journalArticle

37 Citations (Scopus)

Abstract

Diagrammatic reasoning has the potential to be important in numerous
application areas. This paper focuses on the simple, but widely used, Euler diagrams that form the basis of many more expressive logics. We have implemented a diagrammatic theorem prover, called Edith, which has access to four sound and complete sets of reasoning rules for Euler diagrams. Furthermore, for each rule set we develop a sophisticated heuristic to guide the search for a proof. This paper is about understanding how the choice of reasoning rule set affects the time taken to find proofs. Such an understanding will influence reasoning rule design in other logics. Moreover, this work specific to Euler diagrams directly benefits the many logics based on Euler diagrams. We investigate how the time taken to find a proof depends not only on the proof task but also on the reasoning system used. Our evaluation allows us to predict the best choice of reasoning system, given a proof task, in terms of time taken, and we extract a guide for defining reasoning rules for other logics in order to minimize time requirements.
Original languageEnglish
Pages (from-to)431-470
Number of pages40
JournalJournal of Automated Reasoning
Volume39
Issue number4
DOIs
Publication statusPublished - Dec 2007

Fingerprint

Theorem proving
Acoustic waves

Keywords

  • visual languages
  • Euler diagrams
  • diagrammatic reasoning
  • heuristics

Cite this

Automated Theorem Proving in Euler Diagram Systems. / Stapleton, Gem; Masthoff, Judith Francoise Maria; Flower, Jean; Fish, Andrew; Southern, Jane.

In: Journal of Automated Reasoning, Vol. 39, No. 4, 12.2007, p. 431-470.

Research output: Contribution to journalArticle

Stapleton, Gem ; Masthoff, Judith Francoise Maria ; Flower, Jean ; Fish, Andrew ; Southern, Jane. / Automated Theorem Proving in Euler Diagram Systems. In: Journal of Automated Reasoning. 2007 ; Vol. 39, No. 4. pp. 431-470.
@article{8e2198b53fb74a1aad68bd3cd0a72800,
title = "Automated Theorem Proving in Euler Diagram Systems",
abstract = "Diagrammatic reasoning has the potential to be important in numerous application areas. This paper focuses on the simple, but widely used, Euler diagrams that form the basis of many more expressive logics. We have implemented a diagrammatic theorem prover, called Edith, which has access to four sound and complete sets of reasoning rules for Euler diagrams. Furthermore, for each rule set we develop a sophisticated heuristic to guide the search for a proof. This paper is about understanding how the choice of reasoning rule set affects the time taken to find proofs. Such an understanding will influence reasoning rule design in other logics. Moreover, this work specific to Euler diagrams directly benefits the many logics based on Euler diagrams. We investigate how the time taken to find a proof depends not only on the proof task but also on the reasoning system used. Our evaluation allows us to predict the best choice of reasoning system, given a proof task, in terms of time taken, and we extract a guide for defining reasoning rules for other logics in order to minimize time requirements.",
keywords = "visual languages, Euler diagrams, diagrammatic reasoning, heuristics",
author = "Gem Stapleton and Masthoff, {Judith Francoise Maria} and Jean Flower and Andrew Fish and Jane Southern",
year = "2007",
month = "12",
doi = "10.1007/S10817-007-9069-Y",
language = "English",
volume = "39",
pages = "431--470",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer Netherlands",
number = "4",

}

TY - JOUR

T1 - Automated Theorem Proving in Euler Diagram Systems

AU - Stapleton, Gem

AU - Masthoff, Judith Francoise Maria

AU - Flower, Jean

AU - Fish, Andrew

AU - Southern, Jane

PY - 2007/12

Y1 - 2007/12

N2 - Diagrammatic reasoning has the potential to be important in numerous application areas. This paper focuses on the simple, but widely used, Euler diagrams that form the basis of many more expressive logics. We have implemented a diagrammatic theorem prover, called Edith, which has access to four sound and complete sets of reasoning rules for Euler diagrams. Furthermore, for each rule set we develop a sophisticated heuristic to guide the search for a proof. This paper is about understanding how the choice of reasoning rule set affects the time taken to find proofs. Such an understanding will influence reasoning rule design in other logics. Moreover, this work specific to Euler diagrams directly benefits the many logics based on Euler diagrams. We investigate how the time taken to find a proof depends not only on the proof task but also on the reasoning system used. Our evaluation allows us to predict the best choice of reasoning system, given a proof task, in terms of time taken, and we extract a guide for defining reasoning rules for other logics in order to minimize time requirements.

AB - Diagrammatic reasoning has the potential to be important in numerous application areas. This paper focuses on the simple, but widely used, Euler diagrams that form the basis of many more expressive logics. We have implemented a diagrammatic theorem prover, called Edith, which has access to four sound and complete sets of reasoning rules for Euler diagrams. Furthermore, for each rule set we develop a sophisticated heuristic to guide the search for a proof. This paper is about understanding how the choice of reasoning rule set affects the time taken to find proofs. Such an understanding will influence reasoning rule design in other logics. Moreover, this work specific to Euler diagrams directly benefits the many logics based on Euler diagrams. We investigate how the time taken to find a proof depends not only on the proof task but also on the reasoning system used. Our evaluation allows us to predict the best choice of reasoning system, given a proof task, in terms of time taken, and we extract a guide for defining reasoning rules for other logics in order to minimize time requirements.

KW - visual languages

KW - Euler diagrams

KW - diagrammatic reasoning

KW - heuristics

U2 - 10.1007/S10817-007-9069-Y

DO - 10.1007/S10817-007-9069-Y

M3 - Article

VL - 39

SP - 431

EP - 470

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 4

ER -