From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id TAA32178 for caml-redist; Fri, 12 May 2000 19:09:51 +0200 (MET DST) Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id SAA20197 for ; Fri, 12 May 2000 18:19:16 +0200 (MET DST) Received: from orion.inrets.fr (orion.inrets.fr [137.121.1.1]) by nez-perce.inria.fr (8.10.0/8.10.0) with ESMTP id e4CGJEb04108 for ; Fri, 12 May 2000 18:19:15 +0200 (MET DST) Received: from deneb.inrets.fr by orion.inrets.fr (8.9.3/8.7.1); Fri, 12 May 2000 18:19:11 +0200 (MET DST) Received: from terre.inrets.fr by deneb.inrets.fr (8.7.6/8.7.6); Fri, 12 May 2000 18:19:11 +0200 (MET DST) Received: from inrets.fr (localhost [127.0.0.1]) by terre.inrets.fr (8.9.3/8.8.8) with ESMTP id SAA08625 for ; Fri, 12 May 2000 18:19:08 +0200 (MET DST) Sender: weis Message-ID: <391C2EFA.C8037178@inrets.fr> Date: Fri, 12 May 2000 16:19:06 +0000 From: Georges MARIANO Organization: INRETS-ESTAS X-Mailer: Mozilla 4.7 [en] (X11; I; Linux 2.2.12 i686) X-Accept-Language: fr-FR, en MIME-Version: 1.0 To: "caml-list@inria.fr" Subject: looking for "logic calculus" code Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit 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