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.
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
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)