Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <25904-0@swan.cl.cam.ac.uk>; Fri, 17 Jan 1992 17:57:52 +0000 Received: by ted.cs.uidaho.edu. (16.6/1.34) id AA28658; Fri, 17 Jan 92 09:39:00 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu. (16.6/1.34) id AA28654; Fri, 17 Jan 92 09:38:50 -0800 Received: from teal.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl id <25584-0@swan.cl.cam.ac.uk>; Fri, 17 Jan 1992 17:40:50 +0000 To: info-hol@edu.uidaho.cs.ted Subject: Re: "What's out there?" questions Date: Fri, 17 Jan 92 17:40:43 +0000 From: Richard.Boulton@uk.ac.cam.cl Message-Id: <"swan.cl.ca.586:17.00.92.17.40.52"@cl.cam.ac.uk> > Second, have people written decision/proof procedures for Presburger > (sp?) arithmetic, or the theory of <=, or the theory of =, with only > universal quantifiers? The Penelope and Eves provers have such things, > and people here have found them very useful. Is something like them > available for HOL88 and/or HOL90? I have been developing a proof procedure for non-existential Presburger arithmetic (formulae constructed from numeric constants, numeric variables, +, multiplication by constants, <=, <, =, >, >= and first order logical connectives, which when placed in prenex normal form do not contain existential quantifiers). My procedure is for natural number arithmetic, but should be straightforward to port to integers, rationals and reals. The procedure is not complete for naturals or integers but handles most examples you're likely to want in practice. Subtraction is a problem in natural number arithmetic. I haven't handled this yet but hope to. Unfortunately this is just an appetizer (sp?). The procedure is not ready to be released yet. It *might* be ready for the next release of HOL. I am developing it for HOL88, but it should become available for HOL90 as well. Richard Boulton (rjb@cl.cam.ac.uk)