Heterogeneous proofs: spider diagrams meet higher-order provers. (English) Zbl 1342.68305
Van Eekelen, Marko (ed.) et al., Interactive theorem proving. Second international conference, ITP 2011, Berg en Dal, The Netherlands, August 22–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22862-9/pbk). Lecture Notes in Computer Science 6898, 376-382 (2011).
Summary: We present an interactive heterogeneous theorem proving framework, which performs formal reasoning by arbitrarily mixing diagrammatic and sentential proof steps.
We use Isabelle to enable formal reasoning with either traditional sentences or spider diagrams. We provide a mechanisation of the theory of abstract spider diagrams and establish a formal link between diagrammatic concepts and the existing theories in Isabelle/HOL.
For the entire collection see [Zbl 1219.68024].
We use Isabelle to enable formal reasoning with either traditional sentences or spider diagrams. We provide a mechanisation of the theory of abstract spider diagrams and establish a formal link between diagrammatic concepts and the existing theories in Isabelle/HOL.
For the entire collection see [Zbl 1219.68024].
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
References:
| [1] | Barker-Plummer, D., Etchemendy, J., Liu, A., Murray, M., Swoboda, N.: Openproof - A Flexible Framework for Heterogeneous Reasoning. In: Stapleton, G., Howse, J., Lee, J. (eds.) Diagrams 2008. LNCS (LNAI), vol. 5223, pp. 347–349. Springer, Heidelberg (2008) · doi:10.1007/978-3-540-87730-1_32 |
| [2] | Barwise, J., Etchemendy, J.: A Computational Architecture for Heterogeneous Reasoning. In: TARK, pp. 1–11. Morgan Kaufmann, San Francisco (1998) |
| [3] | Gil, J., Howse, J., Kent, S.: Towards a Formalization of Constraint Diagrams. In: IEEE Symposia on Human-Centric Computing Languages and Environments, p. 72 (2001) · doi:10.1109/HCC.2001.995241 |
| [4] | Gordon, M., Wadsworth, C.P., Milner, R.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS, vol. 78. Springer, Heidelberg (1979) · Zbl 0421.68039 · doi:10.1007/3-540-09724-4 |
| [5] | Hammer, E.: Reasoning with Sentences and Diagrams. NDJFL 35(1), 73–87 (1994) · Zbl 0801.03004 |
| [6] | Howse, J., Molina, F., Taylor, J., Kent, S., Gil, J.: Spider Diagrams: A Diagrammatic Reasoning System. JVLC 12(3), 299–324 (2001) |
| [7] | Howse, J., Stapleton, G., Taylor, J.: Spider Diagrams. LMS JCM 8, 145–194 (2005) · Zbl 1074.03006 |
| [8] | Jamnik, M., Bundy, A., Green, I.: On Automating Diagrammatic Proofs of Arithmetic Arguments. JOLLI 8(3), 297–321 (1999) · Zbl 0941.03008 · doi:10.1023/A:1008323427489 |
| [9] | Shin, S.-J.: Heterogeneous Reasoning and its Logic. BSL 10(1), 86–106 (2004) · Zbl 1067.03002 |
| [10] | Stapleton, G., Masthoff, J., Flower, J., Fish, A., Southern, J.: Automated Theorem Proving in Euler Diagram Systems. JAR 39(4), 431–470 (2007) · Zbl 1132.68683 · doi:10.1007/s10817-007-9069-y |
| [11] | Stapleton, G., Taylor, J., Thompson, S., Howse, J.: The expressiveness of spider diagrams augmented with constants. JVLC 20(1), 30 (2009) · Zbl 1401.03031 |
| [12] | Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle Framework. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 33–38. Springer, Heidelberg (2008) · Zbl 1165.68478 · doi:10.1007/978-3-540-71067-7_7 |
| [13] | Winterstein, D., Bundy, A., Gurr, C.: Dr.Doodle: A diagrammatic theorem prover. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 331–335. Springer, Heidelberg (2004) · Zbl 1126.68584 · doi:10.1007/978-3-540-25984-8_24 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
