looking for "logic calculus" code

From: Georges MARIANO (georges.mariano@inrets.fr)
Date: Fri May 12 2000 - 18:19:06 MET DST

  • Next message: Amit Dubey: "Suggestion: Print more error messages?"

    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

    This archive was generated by hypermail 2b29 : Fri May 12 2000 - 19:16:56 MET DST