Formalizing mathematical knowledge as a biform theory graph: a case study
From MaRDI portal
Publication:2364688
DOI10.1007/978-3-319-62075-6_2zbMath1367.68299arXiv1704.02253OpenAlexW2605703278WikidataQ60712705 ScholiaQ60712705MaRDI QIDQ2364688
William M. Farmer, Jacques Carette
Publication date: 21 July 2017
Full work available at URL: https://arxiv.org/abs/1704.02253
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (2)
Formalizing mathematical knowledge as a biform theory graph: a case study ⋮ Incorporating quotation and evaluation into Church's type theory
Uses Software
Cites Work
- Unnamed Item
- A scalable module system
- Mathematical knowledge management: transcending the one-brain-barrier with theory graphs
- Logical number theory I. An introduction
- IMPS: An interactive mathematical proof system
- Theory morphisms in Church's type theory with quotation and evaluation
- Formalizing mathematical knowledge as a biform theory graph: a case study
- Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics
- The Formalization of Syntax-Based Mathematical Algorithms Using Quotation and Evaluation
- Dependently Typed Programming in Agda
- Information Flow
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Biform Theories in Chiron
- Theorem Proving in Higher Order Logics
- High-Level Theories
This page was built for publication: Formalizing mathematical knowledge as a biform theory graph: a case study