Path: utzoo!attcan!uunet!mcsun!ukc!edcastle!aipna!geraint
From: geraint@aipna.ed.ac.uk (Geraint Wiggins)
Newsgroups: comp.lang.prolog
Subject: Re: Theorem Prover
Keywords: Boyer-Moore, Theorem Provers
Message-ID: <1991Feb28.102336@aipna.ed.ac.uk>
Date: 28 Feb 91 10:23:36 GMT
References: <7569@uceng.UC.EDU>
Sender: news@aipna.ed.ac.uk
Reply-To: geraint@aipna.ed.ac.uk (Geraint Wiggins)
Followup-To: comp.lang.prolog
Organization: Dept of AI, University of Edinburgh
Lines: 16

We have a Prolog based theorem prover called Oyster which
we use for our proof planning research work. It is a
reimplementation of Constable et al's NUPRL system in
prolog by Christian Horn. It works in Martin-Lof Constructive
Type Theory and is able to extract programs from proofs
developed in it. 

We distribute Oyster at media cost, along with the current
version of the CLaM proof planner. We are currently working on
a version of the system working in 1st order sorted logic.

Contact Gordon Reid (gordon@uk.ac.ed.ai) for further details.

Hope this helps.

Geraint