Biform theories: project description

DOI10.1007/978-3-319-96812-4_7MaRDI QIDQ1798949zbMATH OpenOpenAlexFDO

Authors Jacques Carette, William M. Farmer, Yasmine Sharoda

Publication date 18 October 2018

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

Mathematics Subject Classification ID

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 specifying and reasoning about algorithms that manipulate mathematical expressions. However, formalizing biform theories is challenging since it requires the means to express statements about the interplay of what these algorithms do and what their actions mean mathematically. This paper describes a project to develop a methodology for expressing, manipulating, managing, and generating mathematical knowledge as a network of biform theories. It is a subproject of MathScheme, a long-term project at McMaster University to produce a framework for integrating formal deduction and symbolic computation.

Recommendations

• Formalizing mathematical knowledge as a biform theory graph: a case study
• An overview of a formal framework for managing mathematics
• Engineering mathematics: the odd order theorem proof
• scientific article; zbMATH DE number 1254246
• scientific article; zbMATH DE number 1405417

Cited in

(6)

• Biform Theories in Chiron
• A synopsis of morphoid type theory
• scientific article; zbMATH DE number 219207 (Why is no real title available?)
• The formalization of group theory knowledge and solving
• Towards the essence of hygiene
• Formalizing mathematical knowledge as a biform theory graph: a case study

Describes a project that uses

Uses Software

• Idris
• Lean
• MathScheme
• Hakaru
• Agda
• HOL Light
• Maple

This page was built for publication: Biform theories: project description

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