Integrating computational and deduction systems using OpenMath

The standard OpenMath is a crucial ingredient for creating an integrated environment combining systems for computer algebra with proof checkers. OpenMath consists of a formal grammar of OpenMath objects, their encodings, Content Dictionaries, Phrasebooks and other tools. The OpenMath standard allows integration of computational systems of different kind. Here we demonstrate how OpenMath works by setting up an environment in which Maple expressions are type-checked by the proof checkers Lego and Coq