Skip to main content
SpringerLink
Log in

Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study

  • Conference paper
  • First Online:
Intelligent Computer Mathematics (CICM 2017)

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

Included in the following conference series:

Abstract

A biform theory is a combination of an axiomatic theory and an algorithmic theory that supports the integration of reasoning and computation. These are ideal for formalizing algorithms that manipulate mathematical expressions. A theory graph is a network of theories connected by meaning-preserving theory morphisms that map the formulas of one theory to the formulas of another theory. Theory graphs are in turn well suited for formalizing mathematical knowledge at the most convenient level of abstraction using the most convenient vocabulary. We are interested in the problem of whether a body of mathematical knowledge can be effectively formalized as a theory graph of biform theories. As a test case, we look at the graph of theories encoding natural number arithmetic. We used two different formalisms to do this, which we describe and compare. The first is realized in \({\textsc {ctt}}_\mathrm{uqe}\), a version of Church’s type theory with quotation and evaluation, and the second is realized in Agda, a dependently typed programming language.

This research was supported by NSERC.

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

Access this chapter

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 EPUB and 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

Institutional subscriptions

Notes

  1. 1.

    As of early 2017, there is no official publication describing these features outside of the Agda documentation, but see [20, 21].

  2. 2.

    It would require us to define paths in terms, bound and free variables along paths, quantification over paths, etc.

References

  1. Aydemir, B.E., et al.: Mechanized metatheory for the masses: the PoplMark challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 50–65. Springer, Heidelberg (2005). doi:10.1007/11541868_4

    Chapter  Google Scholar 

  2. Barwise, J., Seligman, J., Flow, I.: The Logic of Distributed Systems. Tracts in Computer Science, vol. 44. Cambridge University Press, Cambridge (1997)

    MATH  Google Scholar 

  3. Carette, J., Farmer, W.M.: Formalizing mathematical knowledge as a biform theory graph: a case study. arXiv:1704.02253 (2017)

  4. Carette, J., Farmer, W.M.: High-level theories. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) CICM 2008. LNCS, vol. 5144, pp. 232–245. Springer, Heidelberg (2008). doi:10.1007/978-3-540-85110-3_19

    Chapter  Google Scholar 

  5. Farmer, W.M.: Biform theories in Chiron. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Calculemus/MKM -2007. LNCS, vol. 4573, pp. 66–79. Springer, Heidelberg (2007). doi:10.1007/978-3-540-73086-6_6

    Chapter  Google Scholar 

  6. Farmer, W.M.: The formalization of syntax-based mathematical algorithms using quotation and evaluation. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS, vol. 7961, pp. 35–50. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39320-4_3

    Chapter  Google Scholar 

  7. Farmer, W.M.: Incorporating quotation and evaluation into church’s type theory. Computing Research Repository (CoRR) abs/1612.02785, p. 72 (2016)

    Google Scholar 

  8. Farmer, W.M.: Incorporating quotation and evaluation into church’s type theory: syntax and semantics. In: Kohlhase, M., Johansson, M., Miller, B., de Moura, L., Tompa, F. (eds.) CICM 2016. LNCS, vol. 9791, pp. 83–98. Springer, Cham (2016). doi:10.1007/978-3-319-42547-4_7

    Chapter  Google Scholar 

  9. Farmer, W.M.: Theory morphisms in church’s type theory with quotation and evaluation. Computing Research Repository (CoRR) abs/1703.02117, p. 15 (2017)

    Google Scholar 

  10. Farmer, W.M., Guttman, J.D., Javier Thayer, F.: Little theories. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 567–581. Springer, Heidelberg (1992). doi:10.1007/3-540-55602-8_192

    Google Scholar 

  11. Farmer, W.M., Guttman, J.D., Thayer, F.J.: IMPS: an interactive mathematical proof system. J. Autom. Reasoning 11, 213–248 (1993)

    Article  MATH  Google Scholar 

  12. Jenks, R.D., Sutor, R.S.: Axiom: The Scientific Computation System. Springer, Heidelberg (1992)

    MATH  Google Scholar 

  13. Kohlhase, M.: Mathematical knowledge management: transcending the one-brain-barrier with theory graphs. Eur. Math. Soc. (EMS) Newslett. 92, 22–27 (2014)

    MathSciNet  MATH  Google Scholar 

  14. Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Chalmers University of Technology (2007)

    Google Scholar 

  15. Norell, U.: Dependently typed programming in Agda. In: Kennedy, A., Ahmed, A. (eds.) Proceedings of TLDI 2009, pp. 1–2. ACM (2009)

    Google Scholar 

  16. Rabe, F., Kohlhase, M.: A scalable model system. Inf. Comput. 230, 1–54 (2013)

    Article  MATH  Google Scholar 

  17. Smoryński, C.: Logical Number Theory I: An Introduction. Springer, Heidelberg (1991)

    Book  MATH  Google Scholar 

  18. Agda Team: Agda wiki. http://wiki.portal.chalmers.se/agda/pmwiki.php. Accessed 15 May 2017

  19. The Univalent Foundations Theory Program: Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study (2013). https://homotopytypetheory.org/book

  20. van der Walt, P.: Reflection in Agda. Master’s thesis, Universiteit Utrecht, (2012). https://dspace.library.uu.nl/handle/1874/256628

  21. Walt, P., Swierstra, W.: Engineering proof by reflection in Agda. In: Hinze, R. (ed.) IFL 2012. LNCS, vol. 8241, pp. 157–173. Springer, Heidelberg (2013). doi:10.1007/978-3-642-41582-1_10

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computing and Software, McMaster University, Hamilton, Canada

    Jacques Carette & William M. Farmer

Authors
  1. Jacques Carette
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. William M. Farmer
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Jacques Carette or William M. Farmer .

Editor information

Editors and Affiliations

  1. Radboud University, Nijmegen, The Netherlands

    Herman Geuvers

  2. Coventry University, Coventry, United Kingdom

    Matthew England

  3. National University of Sciences and Technology, Islamabad, Pakistan

    Osman Hasan

  4. Jacobs University Bremen, Bremen, Germany

    Florian Rabe

  5. FIZ Karlsruhe, Berlin, Germany

    Olaf Teschke

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Carette, J., Farmer, W.M. (2017). Formalizing Mathematical Knowledge as a Biform Theory Graph: A Case Study. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds) Intelligent Computer Mathematics. CICM 2017. Lecture Notes in Computer Science(), vol 10383. Springer, Cham. https://doi.org/10.1007/978-3-319-62075-6_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-62075-6_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-62074-9

  • Online ISBN: 978-3-319-62075-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation