From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id BAA28586; Sat, 6 Mar 2004 01:50:12 +0100 (MET) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id BAA28503 for ; Sat, 6 Mar 2004 01:50:11 +0100 (MET) Received: from mx.laposte.net (mx.laposte.net [81.255.54.11]) by concorde.inria.fr (8.12.10/8.12.10) with ESMTP id i260oAUM006429 for ; Sat, 6 Mar 2004 01:50:10 +0100 Received: from ensta.org (80.8.57.131) by mx.laposte.net (7.0.024) (authenticated as olivier.grisel) id 4036D2FE004AF41F for caml-list@inria.fr; Sat, 6 Mar 2004 01:50:10 +0100 Message-ID: <404920C0.5010701@ensta.org> Date: Sat, 06 Mar 2004 01:52:16 +0100 From: Olivier Grisel User-Agent: Mozilla/5.0 (X11; U; Linux ppc; en-US; rv:1.6b) Gecko/20031222 Thunderbird/0.4 X-Accept-Language: en-us, en MIME-Version: 1.0 To: caml-list@inria.fr Subject: Re: [Caml-list] Computational Logic in OCaml References: <404612C3.9020603@ensta.org> <16454.58467.587275.600546@gargle.gargle.HOWL> In-Reply-To: <16454.58467.587275.600546@gargle.gargle.HOWL> X-Enigmail-Version: 0.82.5.0 X-Enigmail-Supports: pgp-inline, pgp-mime Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Miltered: at concorde by Joe's j-chkmail ("http://j-chkmail.ensmp.fr")! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; caml-list:01 hash:01 fol:99 logics:01 horn:99 filliatre:01 horn:99 functors:01 atp:99 1.2.4:01 enigmail:01 bindings:01 bindings:01 ocaml:01 ocaml:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk X-Keywords: X-UID: 62 -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Thanks to anybody who gave me references for my problem (on this ML or privately). The JH's TP examples are a great ressource but I find the organisation of the source code a bit unusual and it makes it hard to use it directly as a library... Anyway it is full of good implementation ideas and I might write my own lib based on those ideas. The Coq standard lib seems to be another interesting reference and I will have a deeper look inside to work out which part refer to FOL and which parts refers to other weird logics I have never heard about :o) I will also think about whether or not de Bruijn indices can help in designing data structures for variable bindings in Horn Clauses. thanks again, Olivier Jean-Christophe Filliatre wrote: | Olivier Grisel writes: | |>I plan to write some implementation of classical Inductive Logic |>Programming strategies in OCaml and I would like to know if there exists |>ocaml libraries for computational logic (first order logic) available |>under a free software license. |> |>I would also welcome thanksfully any advice or design guideline on data |>structures for objects such as Horn clauses (datalog or with functors), |>variable bindings and ideas to efficiently implement opertations such as |>resolution and theta-subsumption test. | | | You may be interested in John Harrison's Theorem Proving Examples: | | http://www.cl.cam.ac.uk/users/jrh/atp/index.html | | Regards, -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.2.4 (GNU/Linux) Comment: Using GnuPG with Thunderbird - http://enigmail.mozdev.org iD8DBQFASSDATsBRE+WZ2SARAu52AJwNN50S8PFSxBnT6gqla+t6QaTSnQCfVU7u rSZEt/HPyPGLOi11dhyBYS0= =VGN4 -----END PGP SIGNATURE----- ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners