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 SAA31896; Wed, 3 Mar 2004 18:13:53 +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 SAA32202 for ; Wed, 3 Mar 2004 18:13:51 +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 i23HDmUM030257 for ; Wed, 3 Mar 2004 18:13:50 +0100 Received: from ensta.org (80.8.67.39) by mx.laposte.net (7.0.024) (authenticated as olivier.grisel) id 4044728A0008F4DC for caml-list@inria.fr; Wed, 3 Mar 2004 18:13:48 +0100 Message-ID: <404612C3.9020603@ensta.org> Date: Wed, 03 Mar 2004 18:15:47 +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: [Caml-list] Computational Logic in OCaml 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; hash:01 caml-list:01 horn:99 functors:01 unification:01 citeseer:01 1.2.4:01 enigmail:01 unify:01 bindings:01 ocaml:01 ocaml:01 caml:01 exists:01 olivier:02 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk X-Keywords: X-UID: 36 -----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Dear Caml-List readers, 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. So far I have found an interesting implemantation of Hantao Zhang's linear Robinson unification algorithm (http://abaababa.ouvaton.org/caml/unify.ml) and graph based algorithms for efficient theta-subsumtion test (http://citeseer.nj.nec.com/111654.html) Thanks for any hint ! -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.2.4 (GNU/Linux) Comment: Using GnuPG with Thunderbird - http://enigmail.mozdev.org iD8DBQFARhLDTsBRE+WZ2SARAky9AJ92gUlyc6gyjbIj1nIBq5MrWvW8rQCgk6II ZVgTYE7MS1fwDhJtCpUNg2o= =a2Od -----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