Received: from antares.mcs.anl.gov (mcs.anl.gov [140.221.9.6]) by ra.abo.fi (8.6.10/8.6.10) with ESMTP id QAA07152; Sun, 11 Feb 1996 16:07:17 +0200
Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10)
	id HAA08924 for qed-out; Sun, 11 Feb 1996 07:39:14 -0600
Received: from aohakobe.ipc.chiba-u.ac.jp (aohakobe.ipc.chiba-u.ac.jp [133.82.241.137]) by antares.mcs.anl.gov (8.6.10/8.6.10)  with ESMTP
	id HAA08919 for <qed@mcs.anl.gov>; Sun, 11 Feb 1996 07:39:04 -0600
Received: from aohakobe (localhost [127.0.0.1]) by aohakobe.ipc.chiba-u.ac.jp (8.6.12/3.4Wbeta3 (-: 95041617) with ESMTP id WAA05674 for <qed@mcs.anl.gov>; Sun, 11 Feb 1996 22:40:17 +0900
Message-Id: <199602111340.WAA05674@aohakobe.ipc.chiba-u.ac.jp>
To: qed@mcs.anl.gov
Subject: Re: QED and OpenMath 
In-reply-to: Your message of "Sun, 11 Feb 1996 07:39:51 GMT."
             <5249@campion.demon.co.uk> 
Date: Sun, 11 Feb 1996 22:40:17 +0900
From: Yozo Toda (TELEPHONE +81-43-290-3539) <yozo@aohakobe.ipc.chiba-u.ac.jp>
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


> I am interested to know whether QED participants know about the OpenMath
> intiative and if so what they think about the relevance of OpenMath to QED
> and vice-versa.

As far as I know, OpenMath project aims at developing
the standard notation to share libraries between
many computer algebra systems.

  <A HREF="http://www-f.rrz.uni-koeln.de/themen/Computeralgebra/OpenMath/">
    OpenMath Information Page
  </A>

Thinking about cooperation of computer algebra systems
(like Maple, Mathematica, Reduce, ...) and
provers/proof-checkers/proof-assistants,
there is a chance to share the same notation for mathematical concepts.

But I myself have no experience using both systems, and
I cannot estimate to what extent the issue is important...

-- yozo.