Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

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: -- (:)
From: Olivier Grisel <olivier.grisel@e...>
Subject: [Caml-list] Computational Logic in OCaml
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
( and graph based algorithms
for efficient theta-subsumtion test (

Thanks for any hint !
Version: GnuPG v1.2.4 (GNU/Linux)
Comment: Using GnuPG with Thunderbird -


To unsubscribe, mail Archives:
Bug reports: FAQ:
Beginner's list: