A Microkernel for a Mechanized Mathematics System

William M. Farmer and Martin v. Mohrenschildt

2001

Abstract

A microkernel system is described that provides services for creating
and extending formal languages, theories, computations, deductions,
and interpretations of one theory in another.  In analogy to an
operating system microkernel, this microkernel is a platform for
implementing multiple logics and interpretations between logics.  It
is intended to be the bottom layer of a mechanized mathematics system
that supports the full mathematics process with the capabilities of
both contemporary theorem proving systems and computer algebra
systems.