Abstract
Heterogeneous reasoning refers to theorem proving with mixed diagrammatic and sentential languages and inference steps. We introduce a heterogeneous logic that enables a simple and flexible way to extend logics of existing general-purpose theorem provers with representations from entirely different and possibly not formalised domains. We use our heterogeneous logic in a framework that enables integrating different reasoning tools into new heterogeneous reasoning systems. Our implementation of this framework is MixR – we demonstrate its flexibility and extensibility with a few examples.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
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)
Böhme, S., Nipkow, T.: Sledgehammer: Judgement day. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 107–121. Springer, Heidelberg (2010)
Calcagno, C., Gardner, P., Zarfaty, U.: Context logic as modal logic: completeness and parametric inexpressivity. In: POPL, pp. 123–134. ACM (2007)
Farmer, W.M.: Biform Theories in Chiron. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM/CALCULEMUS 2007. LNCS (LNAI), vol. 4573, pp. 66–79. Springer, Heidelberg (2007)
Giunchiglia, F., Serafini, L.: Multilanguage hierarchical logics, or: How we can do without modal logics. AI 65(1), 29–70 (1994)
Siekmann, J.H., et al.: Proof development with ΩMEGA. In: Voronkov, A. (ed.) CADE-18. LNCS (LNAI), vol. 2392, pp. 144–149. Springer, Heidelberg (2002)
Jamnik, M., Bundy, A., Green, I.: On Automating Diagrammatic Proofs of Arithmetic Arguments. JOLLI 8(3), 297–321 (1999)
Kortenkamp, U., Richter-Gebert, J.: Using automatic theorem proving to improve the usability of geometry software. In: Procedings of the Mathematical User-Interfaces Workshop, pp. 1–12 (2004)
Mossakowski, T., Maeder, C., Lüttich, K.: The Heterogeneous Tool Set, Hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007)
Paulson, L.C.: Isabelle - A Generic Theorem Prover. LNCS, vol. 828. Springer, Heidelberg (1994)
Shin, S.J.: Heterogeneous Reasoning and its Logic. BSL 10(1), 86–106 (2004)
Urbas, M., Jamnik, M.: Diabelli: A heterogeneous proof system. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 559–566. Springer, Heidelberg (2012)
Urbas, M., Jamnik, M., Stapleton, G., Flower, J.: Speedith: A diagrammatic reasoner for spider diagrams. In: Cox, P., Plimmer, B., Rodgers, P. (eds.) Diagrams 2012. LNCS (LNAI), vol. 7352, pp. 163–177. Springer, Heidelberg (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Urbas, M., Jamnik, M. (2014). A Framework for Heterogeneous Reasoning in Formal and Informal Domains. In: Dwyer, T., Purchase, H., Delaney, A. (eds) Diagrammatic Representation and Inference. Diagrams 2014. Lecture Notes in Computer Science(), vol 8578. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44043-8_28
Download citation
DOI: https://doi.org/10.1007/978-3-662-44043-8_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44042-1
Online ISBN: 978-3-662-44043-8
eBook Packages: Computer ScienceComputer Science (R0)