Integrating computational and deduction systems using OpenMath

O. Caprotti, A.M. Cohen

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

3 Citations (Scopus)
1 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationProceedings Calculemus 99 (Trento, Italy, July 1999)
Publication statusPublished - 1999

Publication series

NameElectronic Notes in Theoretical Computer Science
ISSN (Print)1571-0061


Dive into the research topics of 'Integrating computational and deduction systems using OpenMath'. Together they form a unique fingerprint.

Cite this