Helle everyone,

In order to avoid wasting time and development ressources, I'm looking
for ocaml code implementing some aspects of first order logic
and more precisely proof in FOL

I'm interested with predicate calculus, sequent calculus,
simple proof tactics, fresh variables generation, 
[non]-freeness, term substitution, proofs as abstract data types (?),
and so on...

I know that these concepts are easy to implement but I'd prefer 
to reuse clean and already validated (free) code.

It seems to me that there is no pointer on such material in the hump...
(may be I'm wrong...)

(pointers to "literal" material (technical reports) also accepted !!)
??
Thanks in advance
-- 
> Georges MARIANO                 tel: (33) 03 20 43 84 06
> INRETS, 20 rue Elisee Reclus    fax: (33) 03 20 43 83 59
> 59650 Villeneuve d'Ascq         mailto:mariano@terre.inrets.fr
> FRANCE.                         
> http://www3.inrets.fr/Public/ESTAS/Mariano.Georges/
> http://www3.inrets.fr/BUGhome.html         mailto:Bforum@estas1.inrets.fr