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
looking for "logic calculus" code
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2000-05-12 (17:09)
From: Georges MARIANO <georges.mariano@i...>
Subject: looking for "logic calculus" code
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
> FRANCE.