Abstract
Although automated reasoning with diagrams has been possible for some years, tools for diagrammatic reasoning are generally much less sophisticated than their sentential cousins. The tasks of exploring levels of automation and abstraction in the construction of proofs and of providing explanations of solutions expressed in the proofs remain to be addressed. In this paper we take an interactive proof assistant for Euler diagrams, Speedith, and add tactics to its reasoning engine, providing a level of automation in the construction of proofs. By adding tactics to Speedith's repertoire of inferences, we ease the interaction between the user and the system and capture a higher level explanation of the essence of the proof. We analysed the design options for tactics by using metrics which relate to human readability, such as the number of inferences and the amount of clutter present in diagrams. Thus, in contrast to the normal case with sentential tactics, our tactics are designed to not only prove the theorem, but also to support explanation.
Original language  English 

Title of host publication  Proceedings of the 12th Workshop on User Interfaces for Theorem Provers (IJCAR) 
Place of Publication  Online 
Publisher  Open Publishing Association 
Pages  2943 
Number of pages  15 
DOIs  
Publication status  Published  30 Nov 2016 
Event  Proceedings of the 12th Workshop on User Interfaces for Theorem Provers (IJCAR)  Coimbra, Portugal, 2nd July 2016 Duration: 30 Nov 2016 → … 
Publication series
Name  Electronic Proceedings in Theoretical Computer Science 

Conference
Conference  Proceedings of the 12th Workshop on User Interfaces for Theorem Provers (IJCAR) 

Period  30/11/16 → … 
Bibliographical note
© S. Linker, J. Burton & M. Jamnik. This work is licensed under the Creative Commons Attribution LicenseFingerprint
Dive into the research topics of 'Tactical diagrammatic reasoning'. Together they form a unique fingerprint.Profiles

James Burton
Person: Academic