Skip to main content
SpringerLink
Log in
Book cover

International Conference on Intelligent Computer Mathematics

CICM 2011: Intelligent Computer Mathematics pp 107–122Cite as

A Foundational View on Integration Problems

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 6824))

Abstract

The integration of reasoning and computation services across system and language boundaries is a challenging problem of computer science. In this paper, we use integration for the scenario where we have two systems that we integrate by moving problems and solutions between them. While this scenario is often approached from an engineering perspective, we take a foundational view. Based on the generic declarative language MMT, we develop a theoretical framework for system integration using theories and partial theory morphisms. Because MMT permits representations of the meta-logical foundations themselves, this includes integration across logics. We discuss safe and unsafe integration schemes and devise a general form of safe integration.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aczel, P.: On relating type theories and set theories. In: Altenkirch, T., Naraschewski, W., Reus, B. (eds.) TYPES 1998. LNCS, vol. 1657, pp. 1–18. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  2. Asperti, A., Tassi, E.: Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM/CALCULEMUS 2007. LNCS (LNAI), vol. 4573, pp. 146–160. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  3. Bertot, Y., Castéran, P.: Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)

    MATH  Google Scholar 

  4. Benzmüller, C., Paulson, L., Theiss, F., Fietzke, A.: LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 162–170. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  5. Curry, H., Feys, R.: Combinatory Logic. North-Holland, Amsterdam (1958)

    MATH  Google Scholar 

  6. Carette, J., Farmer, W., Wajs, J.: Trustable Communication between Mathematics Systems. In: Hardin, T., Rioboo, R. (eds.) Proceedings of Calculemus, pp. 58–68 (2003)

    Google Scholar 

  7. Cerioli, M., Meseguer, J.: I Borrow Your Logic (Transporting Logical Structures along Maps). Theoretical Computer Science 173, 311–347 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  8. Delahaye, D.: Information Retrieval in a Coq Proof Library Using Type Isomorphisms. In: Coquand, T., Nordström, B., Dybjer, P., Smith, J. (eds.) TYPES 1999. LNCS, vol. 1956, pp. 131–147. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  9. Delahaye, D., Mayero, M.: Dealing with Algebraic Expressions over a Field in Coq using Maple. Journal of Symbolic Computation 39(5), 569–592 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  10. Farmer, W.: Formalizing Undefinedness Arising in Calculus. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 475–489. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  11. Goguen, J., Burstall, R.: Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery 39(1), 95–146 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  12. Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the Association for Computing Machinery 40(1), 143–184 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  13. Howard, W.: The formulas-as-types notion of construction. In: To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pp. 479–490. Academic Press, London (1980)

    Google Scholar 

  14. Hustadt, U., Schmidt, R.: MSPASS: Modal Reasoning by Translation and First-Order Resolution. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS, vol. 1847, pp. 67–71. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  15. Harrison, J., Théry, L.: A Skeptic’s Approach to Combining HOL and Maple. Journal of Automated Reasoning 21, 279–294 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  16. Iancu, M., Rabe, F.: Formalizing Foundations of Mathematics. Mathematical Structures in Computer Science (to appear 2011), http://kwarc.info/frabe/Research/IR_foundations_10.pdf

  17. Kohlhase, M., Rabe, F., Zholudev, V.: Towards MKM in the Large: Modular Representation and Scalable Software Architecture. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P., Rideau, L., Rioboo, R., Sexton, A. (eds.) AISC 2010. LNCS, vol. 6167, pp. 370–384. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  18. Krauss, A., Schropp, A.: A Mechanized Translation from Higher-Order Logic to Set Theory. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 323–338. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  19. Keller, C., Werner, B.: Importing HOL Light into Coq. In: Kaufmann, M., Paulson, L. (eds.) ITP 2010. LNCS, vol. 6172, pp. 307–322. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  20. McLaughlin, S.: An Interpretation of Isabelle/HOL in HOL Light. In: Shankar, N., Furbach, U. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 192–204. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  21. Meier, A.: System Description: TRAMP: Transformation of Machine-Found Proofs into ND-Proofs at the Assertion Level. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 460–464. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  22. Mossakowski, T., Maeder, C., Lüttich, K.: The Heterogeneous Tool Set. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  23. MoWGLI Project Deliverables (2004), http://mowgli.cs.unibo.it/html_no_frames/deliverables/index.html

  24. Meng, J., Paulson, L.: Translating Higher-Order Clauses to First-Order Clauses. Journal of Automated Reasoning 40(1), 35–60 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  25. Naumov, P., Stehr, M., Meseguer, J.: The hOL/NuPRL proof translator (A practical approach to formal interoperability). In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 329–345. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  26. Obua, S., Skalberg, S.: Importing HOL into Isabelle/HOL. In: Shankar, N., Furbach, U. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 298–302. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  27. Pfenning, F., Schürmann, C., Kohlhase, M., Shankar, N., Owre, S.: The Logosphere Project (2003), http://www.logosphere.org/

  28. Rabe, F., Kohlhase, M.: A Scalable Module System, (2011), http://arxiv.org/abs/1105.0548 (under review)

  29. Sorge, V.: Non-trivial Symbolic Computations in Proof Planning. In: Kirchner, H. (ed.) FroCos 2000. LNCS, vol. 1794, pp. 121–135. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  30. Trac, S., Sutcliffe, G., Pease, A.: Integration of the TPTPWorld into SigmaKEE. In: Konev, B., Schmidt, R., Schulz, S. (eds.) Practical Aspects of Automated Reasoning. CEUR Workshop Proceedings, vol. 373 (2008)

    Google Scholar 

  31. Werner, B.: Sets in types, types in sets. In: Abadi, M., Ito, T. (eds.) TACS 1997. LNCS, vol. 1281, pp. 530–546. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  32. Wiedijk, F.: Formal Proof Sketches. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 378–393. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science, Jacobs University, Bremen, DE, Germany

    Florian Rabe & Michael Kohlhase

  2. Department of Computer Science, University of Bologna (IT), Italy

    Claudio Sacerdoti Coen

Authors
  1. Florian Rabe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Kohlhase
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Claudio Sacerdoti Coen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Departments of Computer Science and Mathematics Sciences, University of Bath, BA2 7AY, United Kingdom

    James H. Davenport

  2. Department of Computing and Software, McMaster University, 1280 Main Street West, L8SK1, Hamilton, Ontario, Canada

    William M. Farmer

  3. Institute for Computing and Information Sciences, Radboud University, Heyendaalseweg 135, 6525 AJ, Nijmegen, The Netherlands

    Josef Urban

  4. Department of Computer Science, Jacobs University Bremen, Campus Ring 12, 28759, Bremen, Germany

    Florian Rabe

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Rabe, F., Kohlhase, M., Sacerdoti Coen, C. (2011). A Foundational View on Integration Problems. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds) Intelligent Computer Mathematics. CICM 2011. Lecture Notes in Computer Science(), vol 6824. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22673-1_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-22673-1_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-22672-4

  • Online ISBN: 978-3-642-22673-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation