Re: Theorem Prover

Article View: comp.lang.prolog

Article #1910

#1910

From: Geraint Wiggins
Date: Thu, 28 Feb 1991 10:23

16 lines
1081 bytes

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

Technical Details

Message-ID: <1991Feb28.102336@aipna.ed.ac.uk>

Path: arc1-ca.pugleaf.net!utzoo!attcan!uunet!mcsun!ukc!edcastle!aipna!geraint

References: <7569@uceng.UC.EDU>

Show Full Headers

Complete Article Headers

Path: arc1-ca.pugleaf.net!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

Reply to Parent Message