MathScheme is a project to develop a new approach to mechanized mathematics in which computer algebra and computer theorem proving are merged without sacrificing power or soundness. The first goal of the project is to develop a formal framework that integrates and generalizes symbolic computation and formal deduction. The second project goal is to design and implement a mechanized mathematics system based on the formal framework. The long-range goal is to build, on top of the mechanized mathematics system, an interactive mathematics laboratory that provides an integrated set of tools for facilitating and managing mathematical reasoning.
Keywords for this software
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Ballarin, Clemens: Locales: a module system for mathematical theories (2014)
- Khan-Afshar, Sanaz; Siddique, Umair; Mahmoud, Mohamed Yousri; Aravantinos, Vincent; Seddiki, Ons; Hasan, Osman; Tahar, Sofiène: Formal analysis of optical systems (2014)
- Carette, Jacques; Farmer, William M.; Jeremic, Filip; Maccio, Vincent; O’connor, Russell; Tran, Quang M.: The mathscheme library: some preliminary experiments (2011)
- Carette, Jacques; Farmer, William M.; O’Connor, Russell: MathScheme: project description (2011)
- Davenport, James H. (ed.); Farmer, William M. (ed.); Urban, Josef (ed.); Rabe, Florian (ed.): Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18--23, 2011. Proceedings (2011)
Further publications can be found at: http://www.cas.mcmaster.ca/research/mathscheme/publications.html