{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:10:08Z","timestamp":1725574208061},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540212683"},{"type":"electronic","value":"9783540259312"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-25931-2_17","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T18:34:19Z","timestamp":1294425259000},"page":"166-181","source":"Crossref","is-referenced-by-count":11,"title":["Generating Readable Proofs: A Heuristic Approach to Theorem Proving With Spider Diagrams"],"prefix":"10.1007","author":[{"given":"Jean","family":"Flower","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Judith","family":"Masthoff","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gem","family":"Stapleton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Dahn, B.I., Wolf, A.: Natural language presentation and combination of automatically generated proofs. In: Proc. Frontiers of Combining Systems, Muenchen, Germany, pp. 175\u2013192 (1996)","DOI":"10.1007\/978-94-009-0349-4_9"},{"issue":"3","key":"17_CR2","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1145\/3828.3830","volume":"32","author":"R. Dechter","year":"1985","unstructured":"Dechter, R., Pearl, J.: Generalized best-first search strategies and the optimality of A\u2009\u2217\u2009. Journal of the Association for Computing Machinery\u00a032(3), 505\u2013536 (1985)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1109\/HCC.2003.1260220"},{"key":"17_CR4","volume-title":"Proc. Computing: The Australasian Theory Symposium","author":"J. Flower","year":"2004","unstructured":"Flower, J., Stapleton, G.: Automated Theorem Proving with Spider Diagrams. In: Proc. Computing: The Australasian Theory Symposium, Elsevier science, Amsterdam (2004)"},{"key":"17_CR5","unstructured":"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)"},{"issue":"2","key":"17_CR6","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1109\/TSSC.1968.300136","volume":"4","author":"P.E. Hart","year":"1968","unstructured":"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\u00a04(2), 100\u2013107 (1968)","journal-title":"IEEE Transactions on System Science and Cybernetics"},{"key":"17_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/3-540-46037-3_6","volume-title":"Diagrammatic Representation and Inference","author":"J. Flower","year":"2002","unstructured":"Flower, J., Howse, J.: Generating Euler Diagrams. In: Hegarty, M., Meyer, B., Narayanan, N.H. (eds.) Diagrams 2002. LNCS (LNAI), vol.\u00a02317, pp. 61\u201375. Springer, Heidelberg (2002)"},{"key":"17_CR8","first-page":"402","volume-title":"Proc. IEEE Symposium on Visual Languages (VL 2000)","author":"J. Howse","year":"2000","unstructured":"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\u2013408. IEEE Computer Society Press, Los Alamitos (2000)"},{"key":"17_CR9","volume-title":"Mathematical Reasoning with Diagrams","author":"M. Jamnik","year":"2001","unstructured":"Jamnik, M.: Mathematical Reasoning with Diagrams. CSLI Publications, Stanford (2001)"},{"key":"17_CR10","volume-title":"Artificial intelligence: Structures and strategies for complex problem solving","year":"2002","unstructured":"Luger, G.F. (ed.): Artificial intelligence: Structures and strategies for complex problem solving, 4th edn. Addison Wesley, Reading (2002)","edition":"4"},{"key":"17_CR11","unstructured":"MacKenzie, D.: Computers and the sociology of mathematical proof. In: Proc. 3rd Northern Formal Methods Workshop (1998), \n                  \n                    http:\/\/www1.bcs.org.uk\/DocsRepository\/02700\/2713\/mackenzi.pdf"},{"key":"17_CR12","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/BF00244513","volume":"4","author":"S. Oppacher","year":"1988","unstructured":"Oppacher, S., Suen, S.: HARP: A tableau-based theorem prover. Journal of Automated Reasoning\u00a04, 69\u2013100 (1988)","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR13","volume-title":"Proceedings of Joint AICS 2002 - Calculemus 2002 Conference, Artificial Intelligence, Automated Reasoning and Symbolic Computation","author":"F. Piroi","year":"2002","unstructured":"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), \n                  \n                    http:\/\/www.risc.unilinz.ac.at\/people\/buchberg\/papers\/2002-02-25-A.pdf\n                  \n                  \n                 (accessed August 2003)"},{"key":"17_CR14","volume-title":"The Logical Status of Diagrams","author":"S.-J. Shin","year":"1994","unstructured":"Shin, S.-J.: The Logical Status of Diagrams. Camb. Uni. Press, Cambridge (1994)"},{"key":"17_CR15","unstructured":"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)"},{"key":"17_CR16","unstructured":"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\u2013270 (2003)"},{"key":"17_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25931-2_12","volume-title":"Diagrammatic Representation and Inference","author":"G. Stapleton","year":"2004","unstructured":"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.\u00a02980, Springer, Heidelberg (2004)"},{"key":"17_CR18","first-page":"371","volume-title":"Diagrammatic Representation and Reasoning","author":"N. Swoboda","year":"2001","unstructured":"Swoboda, N.: Implementing Euler\/Venn reasoning systems. In: Anderson, M., Meyer, B., Oliver, P. (eds.) Diagrammatic Representation and Reasoning, pp. 371\u2013386. Springer, Heidelberg (2001)"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"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.\u00a072(3) (2003)","DOI":"10.1016\/S1571-0661(04)80613-3"},{"key":"17_CR20","unstructured":"The Visual Modelling Group website, \n                  \n                    http:\/\/www.cmis.brighton.ac.uk\/research\/vmg"},{"key":"17_CR21","unstructured":"The Visual Modelling Group technical report on spider diagram reasoning systems at \n                  \n                    http:\/\/www.cmis.brighton.ac.uk\/research\/vmg\/SDRules.html"},{"key":"17_CR22","unstructured":"Windsteiger, W.: An automated prover for Zermelo-Fraenkel set theory in Theorema. LMCS (2002)"}],"container-title":["Lecture Notes in Computer Science","Diagrammatic Representation and Inference"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-25931-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T09:46:13Z","timestamp":1553334373000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-25931-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540212683","9783540259312"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-25931-2_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}