Formalizing mathematical knowledge as a biform theory graph: a case study

DOI10.1007/978-3-319-62075-6_2MaRDI QIDQ2364688zbMATH OpenOpenAlexWikidataFDO

Authors Jacques Carette, William M. Farmer

Publication date 21 July 2017

Full work available at URL https://arxiv.org/abs/1704.02253

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) First-order arithmetic and fragments (03F30) Knowledge representation (68T30)

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 ${mCTT}_{muqe}$, a version of Church's type theory with quotation and evaluation, and the second is realized in Agda, a dependently typed programming language.

Recommendations

• A universal machine for biform theory graphs
• Biform Theories in Chiron
• Biform theories: project description
• A formal framework for managing mathematics
• An overview of a formal framework for managing mathematics

Cites work

• A scalable module system
• Biform Theories in Chiron
• Dependently typed programming in Agda
• Formalizing mathematical knowledge as a biform theory graph: a case study
• High-Level Theories
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 107769 (Why is no real title available?)
• IMPS: An interactive mathematical proof system
• Incorporating quotation and evaluation into Church's type theory: syntax and semantics
• Information Flow
• Logical number theory I. An introduction
• Mathematical knowledge management: transcending the one-brain-barrier with theory graphs
• The formalization of syntax-based mathematical algorithms using quotation and evaluation
• Theorem Proving in Higher Order Logics
• Theory morphisms in Church's type theory with quotation and evaluation

Cited in

(9)

• Knowledge representation for mathematical discovery: Three experiments in graph theory
• Incorporating quotation and evaluation into Church's type theory
• Biform theories: project description
• An overview of a formal framework for managing mathematics
• Formalizing mathematical knowledge as a biform theory graph: a case study
• A formal framework for managing mathematics
• A universal machine for biform theory graphs
• Morphism equality in theory graphs
• Formal entity graphs as complex networks: assessing centrality metrics of the archive of formal proofs

Describes a project that uses

Uses Software

• PoplMark
• AXIOM
• Agda
• IMPS

This page was built for publication: Formalizing mathematical knowledge as a biform theory graph: a case study

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2364688)