coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]logic programming

From: "Nathan Whitehead" <nwhitehe AT gmail.com>
To: "Sean McLaughlin" <seanmcl AT cmu.edu>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club]logic programming
Date: Wed, 25 Oct 2006 12:48:55 -0700
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:reply-to:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=rJvmfiBrpcbGR1TJwioi5a4Ntx4TXQjfTdN26RnyFDuOC3Kt/IDqH9sz57bMXXjrScNPpZOlgknn5K48D4v7Z+Fxk75QscTLBefV5a9z1N5r1C/+0RmLiWNnITs8prqIh9Iq8t64gxRSlQDUObELYzGkONx37UEN6itm1RD+jTE=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

I've coded up Datalog and proved decidability as part of some work on
security logics.  It's available on my homepage at
http://www.soe.ucsc.edu/~nwhitehe in case you find it useful.

A while ago I formalized pure Prolog, but didn't prove anything about
it or develop any algorithms or resolution strategies.  Basically all
it was for was encoding proofs that a goal succeeds against a program.
The proof had to supply all the substitutions, so it didn't even
include unification.  If you want I can put that up too (although it
is easy to reproduce).
--
Nathan Whitehead

[Coq-Club]logic programming, Sean McLaughlin
- Re: [Coq-Club]logic programming, G�rard Huet
- Re: [Coq-Club]logic programming, Nathan Whitehead
- <Possible follow-ups>
- Re: [Coq-Club]logic programming, Thery Laurent