zbMATH — the first resource for mathematics

A universal machine for biform theory graphs. (English) Zbl 1278.68267
Carette, Jacques (ed.) et al., Intelligent computer mathematics. MKM, Calculemus, DML, and systems and projects 2013, held as part of CICM 2013, Bath, UK, July 8–12, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39319-8/pbk). Lecture Notes in Computer Science 7961. Lecture Notes in Artificial Intelligence, 82-97 (2013).
Summary: 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 MMT/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 workflows 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.
For the entire collection see [Zbl 1268.68008].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T30 Knowledge representation
68W30 Symbolic computation and algebraic computation
Full Text: DOI