Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 11 Oct 1993 15:53:46 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA06800; Mon, 11 Oct 93 06:42:10 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from wasa.shh.fi by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA06796; Mon, 11 Oct 93 06:42:07 -0700 Received: from charon.wasa.shh.fi by wasa.shh.fi (4.1/291091(up)) id AA05849; Mon, 11 Oct 93 15:39:38 +0200 Received: From PAMIR/WORKQUEUE by charon.wasa.shh.fi via Charon-4.0A-VROOM with IPX id 100.931011154216.416; 11 Oct 93 15:41:34 +0500 Message-Id: To: info-hol@cs.uidaho.edu From: jwright@wasa.shh.fi Organization: Swedish School of Econ. Vasa Date: 11 Oct 1993 15:38:55 EET Subject: Explaining a contribution Priority: normal X-Mailer: Pegasus Mail/Mac v2.02 Last week I announced a contribution called HOLproof on the theme of Representing higher order logic proofs in HOL Tim Leonard suggested I'd send a three-sentence explanation of what this is all about. Here it is: I've defined new types corresponding to types, terms, sequents and primitive inferences of higher order logic and defined a number of properties (e.g., what it means for a variable to free in a term, for a term to be well-typed and for a list of inferences to be a proof). I have also written some ML code that performs proof checking by doing a proof (i.e., you can input a list L of inferences and the output is either the theorem |- Is_proof L or the theorem |- ~Is_proof L). Finally, I have also formalised the notion of a derived inference rule and proved the correctness of a few of the derived inference rules that the HOL system uses. Joakim von Wright