A Universal Machine for Biform Theory Graphs

TL;DR

This paper introduces a formal, modular framework for biform theory graphs that unify proof and computation systems, enabling automated evaluation of mathematical expressions through shared specifications and implementations.

Contribution

It develops a universal machine for biform theories within the MMTt/OMDoc framework, integrating logic and programming language semantics for enhanced knowledge management.

Findings

Successfully integrated implementations into OpenMath content dictionaries.

Demonstrated automated evaluation of expressions using the biform theory framework.

Provided a modular, formal approach to unify proof and computation systems.

Abstract

Broadly speaking, there are two kinds of semantics-aware assistant systems for mathematics: proof assistants express the semantic in logic and emphasize deduction, and computer algebra systems express the semantics in programming languages and emphasize computation. Combining the complementary strengths of both approaches while mending their complementary weaknesses has been an important goal of the mechanized mathematics community for some time. We pick up on the idea of biform theories and interpret it in the MMTt/OMDoc framework which introduced the foundations-as-theories approach, and can thus represent both logics and programming languages as theories. This yields a formal, modular framework of biform theory graphs which mixes specifications and implementations sharing the module system and typing information. We present automated knowledge management work flows that interface to existing specification/programming tools and enable an OpenMath Machine, that operationalizes biform theories, evaluating expressions by exhaustively applying the implementations of the respective operators. We evaluate the new biform framework by adding implementations to the OpenMath standard content dictionaries.