caa a22 4500 46318291X CHVBK 20180406164844.0 cr unu---uuuuu 170326e20071201xx s 000 0 eng 10.1007/s10817-007-9069-y doi (NATIONALLICENCE)springer-10.1007/s10817-007-9069-y Automated Theorem Proving in Euler Diagram Systems [Elektronische Daten] [Gem Stapleton, Judith Masthoff, Jean Flower, Andrew Fish, Jane Southern] 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. Springer Science+Business Media, Inc., 2007 Visual languages nationallicence Euler diagrams nationallicence Diagrammatic reasoning nationallicence Heuristics nationallicence Stapleton Gem Visual Modelling Group, University of Brighton, Brighton, UK aut Masthoff Judith University of Aberdeen, Aberdeen, UK aut Flower Jean Visual Modelling Group, University of Brighton, Brighton, UK aut Fish Andrew Visual Modelling Group, University of Brighton, Brighton, UK aut Southern Jane Visual Modelling Group, University of Brighton, Brighton, UK aut Journal of Automated Reasoning Springer Netherlands 39/4(2007-12-01), 431-470 0168-7433 39:4<431 2007 39 10817 https://doi.org/10.1007/s10817-007-9069-y text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10817-007-9069-y text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Stapleton Gem Visual Modelling Group, University of Brighton, Brighton, UK aut NATIONALLICENCE 700 1- Masthoff Judith University of Aberdeen, Aberdeen, UK aut NATIONALLICENCE 700 1- Flower Jean Visual Modelling Group, University of Brighton, Brighton, UK aut NATIONALLICENCE 700 1- Fish Andrew Visual Modelling Group, University of Brighton, Brighton, UK aut NATIONALLICENCE 700 1- Southern Jane Visual Modelling Group, University of Brighton, Brighton, UK aut NATIONALLICENCE 773 0- Journal of Automated Reasoning Springer Netherlands 39/4(2007-12-01), 431-470 0168-7433 39:4<431 2007 39 10817 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer