[Caml-list] Computational Logic in OCaml

[Caml-list] Computational Logic in OCaml

[Olivier Grisel]

-----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

Re: [Caml-list] Computational Logic in OCaml

[Jean-Christophe Filliatre]

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,
-- 
Jean-Christophe

-------------------
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

Re: [Caml-list] Computational Logic in OCaml

[Olivier Grisel]

-----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