Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 24 May 1994 09:44:30 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA01778; Tue, 24 May 1994 02:43:23 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA01772; Tue, 24 May 1994 02:43:15 -0600 Received: from merganser.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 24 May 1994 09:42:56 +0100 To: hol2000@leopard.cs.byu.edu Subject: Re: hol2000 is very silent In-Reply-To: Your message of "Tue, 24 May 94 10:13:52 +0200." <199405240813.AA02815@borneo.gmd.de> Date: Tue, 24 May 94 09:42:50 +0100 From: Richard Boulton Message-Id: <"swan.cl.cam.:152760:940524084306"@cl.cam.ac.uk> Matthew Morley writes: > Think of the positive benefits a real theorem > proving environment could bring. Doesn't this just > emphasise the point Peter Andrews raised at last > year's HUG about portability of proofs and > theorems and developing interfaces between tools? > I didn't get the impression at the time that > HOLers took that discussion very seriously, but in > my opinion (it's just that) this ought to be if > not at the forefront at least in the vanguard of > any future initiatives in the development of > theorem proving technology. I agree that this is an important issue, though it goes beyond the scope of hol2000 in that it requires a standard to be reached between all the major theorem-prover developers. However, I do think it is legitimate to discuss it here. I saw the following on comp.doc.techreports yesterday. Would anyone like to download a copy and assess its relevance to the interfacing of theorem provers? Richard Boulton. comp.doc.techreports (moderated) #508 From: Marie-Helene Comte Subject: INRIA-Sophia Antipolis New Research Reports Date: Fri May 20 19:55:41 BST 1994 Organization: I.N.R.I.A. , Valbonne Sophia Antipolis, FR Lines: 267 I N R I A ( National Institute for Research in Computer Science and Control) Unite de recherche de Sophia Antipolis INRIA-SOPHIA ANTIPOLIS Technical reports The following technical reports are available in electronical version : - in Postscript format, by ftp anonymous on : zenon.inria.fr , directory /pub/rapports ftp.inria.fr , directory /INRIA/publication/RR or RT - in dvi or Postscript format, with WAIS (full-text reports are indexed) name : ra-zenon-inria-fr.src (DVI format) serveur : zenon.inria.fr service : 210 database : ra-zenon-inria-fr cost : 0 units : :free maintainer : root@zenon.inria.fr name : ra-mime-zenon-inria-fr.src ( MIME format including serveur : zenon.inria.fr abstract and Postscript service : 210 file) database : ra-mime-zenon-inria-fr cost : 0 units : :free maintainer : doc@zenon.inria.fr ---------------------------------------------------------------------- RT-162 Stephane Dalmas, Marc Gaetano, Alain Sausse : ASAP a protocol for symbolic computation systems ASAP un protocole pour des systemes de calcul formel March 1994 In english This report describes the conception and the implementation of a simple protocol for exchanging mathematical data between processes. Our purpose is to enable symbolic computation systems to communicate and cooperate together but also with user programs, graphical interfaces, curve and surface plotters. In the first part, we study the general problem of the exchanging of mathematical data. The second part defines the protocol. Then, we present the documentation of a C library which implements ASAP. Ce rapport decrit la conception de l'implementation d'un protocole simple permettant l'echange de donnees mathematiques entre deux processus. Notre but est de faire communiquer des systemes de calcul formel entre eux mais aussi avec des programmes utilisateurs, des interfaces graphiques, des traceurs de courbes et de surfaces, etc... Dans la premiere partie, on etudie le probleme general de l'echange de donnees mathematiques. La deuxieme partie definit le protocole. Enfin, on presente la documentation d'une bibliotheque de fonctions C qui implemente ASAP.