English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
[Caml-list] Computational Logic in OCaml
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2004-03-06 (00:50)
From: Olivier Grisel <olivier.grisel@e...>
Subject: Re: [Caml-list] Computational Logic in OCaml
Hash: SHA1

Thanks to anybody who gave me references for my problem (on this ML or

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,

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,
Version: GnuPG v1.2.4 (GNU/Linux)
Comment: Using GnuPG with Thunderbird - http://enigmail.mozdev.org


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