Abstract
An important aim of diagrammatic reasoning is to make it easier for people to create and understand logical arguments. We have worked on spider diagrams, which visually express logical statements. Ideally, automatically generated proofs should be short and easy to understand. An existing proof generator for spider diagrams successfully writes proofs, but they can be long and unwieldy. In this paper, we present a new approach to proof writing in diagrammatic systems, which is guaranteed to find shortest proofs and can be extended to incorporate other readability criteria. We apply the A * algorithm and develop an admissible heuristic function to guide automatic proof construction. We demonstrate the effectiveness of the heuristic used. The work has been implemented as part of a spider diagram reasoning tool.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Dahn, B.I., Wolf, A.: Natural language presentation and combination of automatically generated proofs. In: Proc. Frontiers of Combining Systems, Muenchen, Germany, pp. 175–192 (1996)
Dechter, R., Pearl, J.: Generalized best-first search strategies and the optimality of A ∗ . Journal of the Association for Computing Machinery 32(3), 505–536 (1985)
Fish, A., Flower, J., Howse, J.: A Reading algorithm for constraint diagrams. In: Proc. IEEE Symposium on Visual Languages and Formal Methods, New Zealand (2003)
Flower, J., Stapleton, G.: Automated Theorem Proving with Spider Diagrams. In: Proc. Computing: The Australasian Theory Symposium, Elsevier science, Amsterdam (2004)
Goller, C.: Learning search-control heuristics for automated deduction systems with folding architecture networks. In: Proc. European Symposium on Artificial Neural Networks. D-Facto publications (April 1999)
Hart, P.E., Nilsson, N.J., Raphael, B.: A formal basis for the heuristic determination of minimum cost paths. IEEE Transactions on System Science and Cybernetics 4(2), 100–107 (1968)
Flower, J., Howse, J.: Generating Euler Diagrams. In: Hegarty, M., Meyer, B., Narayanan, N.H. (eds.) Diagrams 2002. LNCS (LNAI), vol. 2317, pp. 61–75. Springer, Heidelberg (2002)
Howse, J., Molina, F., Taylor, J.: SD2: A sound and complete diagrammatic reasoning system. In: Proc. IEEE Symposium on Visual Languages (VL 2000), pp. 402–408. IEEE Computer Society Press, Los Alamitos (2000)
Jamnik, M.: Mathematical Reasoning with Diagrams. CSLI Publications, Stanford (2001)
Luger, G.F. (ed.): Artificial intelligence: Structures and strategies for complex problem solving, 4th edn. Addison Wesley, Reading (2002)
MacKenzie, D.: Computers and the sociology of mathematical proof. In: Proc. 3rd Northern Formal Methods Workshop (1998), http://www1.bcs.org.uk/DocsRepository/02700/2713/mackenzi.pdf
Oppacher, S., Suen, S.: HARP: A tableau-based theorem prover. Journal of Automated Reasoning 4, 69–100 (1988)
Piroi, F., Buchberger, B.: Focus windows: A new technique for proof presentation. In: Calmet, J., Benhamou, B., Caprotti, O., Henocque, L., Sorge, V. (eds.) Proceedings of Joint AICS 2002 - Calculemus 2002 Conference, Artificial Intelligence, Automated Reasoning and Symbolic Computation, Marseille, France, July 2002, Springer, Heidelberg (2002), http://www.risc.unilinz.ac.at/people/buchberg/papers/2002-02-25-A.pdf (accessed August 2003)
Shin, S.-J.: The Logical Status of Diagrams. Camb. Uni. Press, Cambridge (1994)
Schumann, J., Robinson, P.: [] or SUCCESS is not enough: Current technology and future directions in proof presentation. In: Proc. IJCAR workshop: Future directions in automated reasoning (2001)
Stapleton, G., Howse, J., Taylor, J.: A constraint diagram reasoning system. In: Proc. International conference on Visual Languages and Computing, Knowledge systems institute, pp. 263–270 (2003)
Stapleton, G., Howse, J., Taylor, J., Thompson, S.: What can spider diagrams say? In: Blackwell, A.F., Marriott, K., Shimojima, A. (eds.) Diagrams 2004. LNCS (LNAI), vol. 2980, Springer, Heidelberg (2004)
Swoboda, N.: Implementing Euler/Venn reasoning systems. In: Anderson, M., Meyer, B., Oliver, P. (eds.) Diagrammatic Representation and Reasoning, pp. 371–386. Springer, Heidelberg (2001)
Swoboda, N., Allwein, G.: Using DAG Transformations to Verify Euler/Venn Homogeneous and Euler/Venn FOL Heterogeneous Rules of Inference. Electronic Notes in Theoretical Computer Science, vol. 72(3) (2003)
The Visual Modelling Group website, http://www.cmis.brighton.ac.uk/research/vmg
The Visual Modelling Group technical report on spider diagram reasoning systems at http://www.cmis.brighton.ac.uk/research/vmg/SDRules.html
Windsteiger, W.: An automated prover for Zermelo-Fraenkel set theory in Theorema. LMCS (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Flower, J., Masthoff, J., Stapleton, G. (2004). Generating Readable Proofs: A Heuristic Approach to Theorem Proving With Spider Diagrams. In: Blackwell, A.F., Marriott, K., Shimojima, A. (eds) Diagrammatic Representation and Inference. Diagrams 2004. Lecture Notes in Computer Science(), vol 2980. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-25931-2_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-25931-2_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21268-3
Online ISBN: 978-3-540-25931-2
eBook Packages: Springer Book Archive