From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id BAA04956; Wed, 21 May 2003 01:57:49 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id BAA04949 for ; Wed, 21 May 2003 01:57:48 +0200 (MET DST) Received: from caduceus.fm.intel.com (fmr02.intel.com [192.55.52.25]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id h4KNvlH23266 for ; Wed, 21 May 2003 01:57:47 +0200 (MET DST) Received: from petasus.fm.intel.com (petasus.fm.intel.com [10.1.192.37]) by caduceus.fm.intel.com (8.11.6p2/8.11.6/d: outer.mc,v 1.57 2003/05/13 17:32:58 rfjohns1 Exp $) with ESMTP id h4KNoA324775 for ; Tue, 20 May 2003 23:50:10 GMT Received: from fmsmsxvs041.fm.intel.com (fmsmsxvs041.fm.intel.com [132.233.42.126]) by petasus.fm.intel.com (8.11.6p2/8.11.6/d: inner.mc,v 1.32 2003/05/13 23:13:25 rfjohns1 Exp $) with SMTP id h4KNpIk24896 for ; Tue, 20 May 2003 23:51:18 GMT Received: from FMSMSX017.fm.intel.com ([132.233.42.196]) by fmsmsxvs041.fm.intel.com (NAVGW 2.5.2.11) with SMTP id M2003052016544606463 for ; Tue, 20 May 2003 16:54:46 -0700 Received: by fmsmsx017.fm.intel.com with Internet Mail Service (5.5.2653.19) id ; Tue, 20 May 2003 16:57:45 -0700 Message-ID: From: "Harrison, John R" To: "'caml-list@inria.fr'" Cc: "Harrison, John R" Subject: [Caml-list] Theorem proving example code available Date: Tue, 20 May 2003 16:57:44 -0700 MIME-Version: 1.0 X-Mailer: Internet Mail Service (5.5.2653.19) Content-Type: text/plain; charset="ISO-8859-1" X-Spam: no; 0.00; johnh:01 model:01 atp:99 emitted:01 threading:01 abstraction:01 ocaml:01 caml:01 closure:01 checking:01 simpler:01 syntax:02 binary:02 rewriting:02 theorem:02 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk I've made available some simple implementations of common automated theorem proving methods. This code, intended to accompany a textbook on theorem proving, is written in Objective CAML and covers quite a range of techniques, e.g. * The Davis-Putnam procedure * Stalmarck's method * Binary decision diagrams * Tableaux * Resolution * Model elimination * Congruence closure * Rewriting * Knuth-Bendix completion * Brand's transformation * Paramodulation * Quantifier elimination over Z, C and R * Groebner bases * Geometry theorem proving * The Nelson-Oppen combination method * CTL and LTL model checking * Symbolic trajectory evaluation * Interactive LCF proof * Mizar-like proofs For more details, and to browse or download the code, see: http://www.cl.cam.ac.uk/users/jrh/atp/index.html The code is intended to illustrate the techniques described in the simplest way I could think of, and *not* to be efficient or practically useful. Part of my aim in making it available is to solicit ideas about how it might be made simpler and clearer. Any suggestions will be gratefully received at . I might mention two notable features of the code as it stands: o The code is entirely functional (well, excluding various status messages that are emitted). In fact, I cheekily redefine the OCaml assignment operator ":=". On the whole, this seems fine, except for some messiness when threading BDD state (e.g. the files "bdd.ml" and "model.ml"). o To represent sets, I use canonically ordered lists. This is questionable both on grounds of abstraction and efficiency, but there is a certain convenience in having an easy concrete syntax and being able to pick out elements by pattern matching. John. ------------------- 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