Browse thread
[Caml-list] Computational Logic in OCaml
-
Olivier Grisel
-
Jean-Christophe Filliatre
- Olivier Grisel
-
Jean-Christophe Filliatre
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ 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 |
-----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