Received: from leopard.cs.byu.edu (leopard.cs.byu.edu [128.187.2.182]) by ra.abo.fi (8.6.10/8.6.10) with ESMTP id PAA18810; Fri, 9 Feb 1996 15:39:01 +0200 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA088038794; Fri, 9 Feb 1996 05:26:34 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: list Received: from bescot.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.37.109.15/16.2) id AA088008780; Fri, 9 Feb 1996 05:26:20 -0700 Received: from woodcock.cl.cam.ac.uk [128.232.2.209] (pc) by bescot.cl.cam.ac.uk with esmtp (Exim 0.37 #2) id E0tkrtx-0001Ns-00; Fri, 9 Feb 1996 12:26:09 +0000 X-Mailer: exmh version 1.6.4+cl+patch 10/10/95 To: info-hol@leopard.cs.byu.edu Cc: Paul.Curzon@cl.cam.ac.uk, reetz Subject: Re: RE2: hol90 should have more control about proofs ... databases In-Reply-To: Your message of "Fri, 09 Feb 1996 11:04:17 +0100." <"iraun1.ira.536:09.02.96.10.05.07"@ira.uka.de> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Fri, 09 Feb 1996 12:25:47 +0100 From: Paul Curzon Message-Id: To branch out on a slightly different tack ... has anyone done any work looking at building a theorem prover on top of a general purpose (eg a commercial relational) database system to manage theories etc? Would this be a sensible thing to try? I believe Albert Camilleri has suggested something like this in the past, but I haven't heard of it having been attempted. This would potentially allow multiple users to work cooperatively on a single project, sharing results etc. If this were done, the problems of visualizing and maintaining proofs would possibly become even more acute since users would be working with other people's possibly dynamically changing theories. Paul. -- Paul Curzon, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, United Kingdom. Telephone: +44 1223 334688, Fax: +44 1223 334678 Email: Paul.Curzon@cl.cam.ac.uk, URL: http://www.cl.cam.ac.uk/users/pc/