TY - GEN
T1 - Integrating computational and deduction systems using OpenMath
AU - Caprotti, O.
AU - Cohen, A.M.
PY - 1999
Y1 - 1999
N2 - 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.
AB - 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.
U2 - 10.1016/S1571-0661(05)80616-4
DO - 10.1016/S1571-0661(05)80616-4
M3 - Conference contribution
T3 - Electronic Notes in Theoretical Computer Science
SP - 469
EP - 480
BT - Proceedings Calculemus 99 (Trento, Italy, July 1999)
ER -