From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=AWL autolearn=disabled version=3.1.3 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 8B674BC69 for ; Thu, 12 Apr 2007 01:55:23 +0200 (CEST) Received: from mga02.intel.com (mga02.intel.com [134.134.136.20]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l3BNtLve016064 for ; Thu, 12 Apr 2007 01:55:22 +0200 Received: from orsmga001.jf.intel.com ([10.7.209.18]) by mga02.intel.com with ESMTP; 11 Apr 2007 16:55:20 -0700 Received: from orsmsx334.jf.intel.com ([10.22.226.45]) by orsmga001.jf.intel.com with ESMTP; 11 Apr 2007 16:55:20 -0700 X-ExtLoop1: 1 X-IronPort-AV: i="4.14,397,1170662400"; d="scan'208"; a="225928416:sNHT30989721" Received: from orsmsx419.amr.corp.intel.com ([10.22.226.88]) by orsmsx334.jf.intel.com with Microsoft SMTPSVC(6.0.3790.1830); Wed, 11 Apr 2007 16:55:20 -0700 X-MimeOLE: Produced By Microsoft Exchange V6.5 Content-class: urn:content-classes:message MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable Subject: RE: [Caml-list] Implementation of a prover Date: Wed, 11 Apr 2007 16:55:19 -0700 Message-ID: <509223F0BF55E74FA1247D17207E7A0C014E571E@orsmsx419.amr.corp.intel.com> In-Reply-To: <53c655920703121441k5004991et194b046ebb601a8a@mail.gmail.com> X-MS-Has-Attach: X-MS-TNEF-Correlator: Thread-Topic: [Caml-list] Implementation of a prover Thread-Index: Acdk77EJHiRzwYqiQE2MB9kMKByFvwXo3LEQ From: "Harrison, John R" To: Cc: X-OriginalArrivalTime: 11 Apr 2007 23:55:20.0727 (UTC) FILETIME=[DCF31270:01C77C94] X-Miltered: at concorde with ID 461D7569.005 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; depth-first:01 model:01 inference:01 ocaml:01 ocaml:01 structurally:01 prolog:01 closures:01 closures:01 caml-list:01 writes:01 algorithm:01 algorithm:01 closure:01 argument:02 David Baelde writes: | There are well-known implementation techniques for | depth-first theorem proving, using continuation-passing | style (success/failure continuations). But these techniques | do not easily allow the building of a proof witness. This is | nice when you have a working proof-search procedure but not | when you're still playing with a logic, trying to find the | right procedure or more generally when you just want an | interactive prover. I don't know exactly what theorem-proving algorithm you have in mind, but I guess you mean some "top down" method like free variable tableaux, Prolog or model elimination. An approach that I've found effective is to pass along a closure that will create the proof when applied to a suitable argument (e.g. the final instantiation of the free variables). In an algorithm where you explore a large search space but eventually get a small proof, you postpone any real proof construction until it's useful, not just an intermediate result in a failed branch. This is particularly valuable if your inference process is relatively expensive, as in a traditional LCF-style prover. Of course, an alternative is just to pass along some simple concrete data structure like a tree. Again this fits easily into the continuation-passing style. But closures can be a bit more flexible, and OCaml seems to handle closures very efficiently, so one needn't be afraid to use them. You can find an example in the code on my Web page, with a proof-less tableau prover "tableau" here: http://www.cl.cam.ac.uk/~jrh13/atp/OCaml/tableaux.ml and a proof-producing "tableau" function here: http://www.cl.cam.ac.uk/~jrh13/atp/OCaml/checking.ml You can see that they are structurally very close. John.