Integrating computational and deduction systems using OpenMath

O. Caprotti, A.M. Cohen

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

3 Citaten (Scopus)
1 Downloads (Pure)

Samenvatting

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.
Originele taal-2Engels
TitelProceedings Calculemus 99 (Trento, Italy, July 1999)
Pagina's469-480
DOI's
StatusGepubliceerd - 1999

Publicatie series

NaamElectronic Notes in Theoretical Computer Science
Volume23
ISSN van geprinte versie1571-0061

Vingerafdruk Duik in de onderzoeksthema's van 'Integrating computational and deduction systems using OpenMath'. Samen vormen ze een unieke vingerafdruk.

  • Citeer dit

    Caprotti, O., & Cohen, A. M. (1999). Integrating computational and deduction systems using OpenMath. In Proceedings Calculemus 99 (Trento, Italy, July 1999) (blz. 469-480). (Electronic Notes in Theoretical Computer Science; Vol. 23). https://doi.org/10.1016/S1571-0661(05)80616-4