Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Thu, 26 Nov 1992 17:27:01 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA13053; Thu, 26 Nov 92 09:14:38 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from nene.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA13048; Thu, 26 Nov 92 09:14:27 -0800 Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by nene.cl.cam.ac.uk with SMTP (PP-6.3) to cl; Thu, 26 Nov 1992 17:11:28 +0000 To: info-hol@edu.uidaho.cs.ted Cc: Tom.Melham@uk.ac.cam.cl Subject: technical report available by FTP. Date: Thu, 26 Nov 92 17:11:19 +0000 From: Tom Melham Message-Id: <"nene.cl.ca.999:26.11.92.17.11.35"@cl.cam.ac.uk> I have made the technical report on inductive definitions available by ftp from ftp.cl.cam.ac.uk in the directory /hvg/papers. The relevant file is called RuleInduction.ps.Z. The details are: Reasoning with Inductively Defined Relations in the HOL Theorem Prover Juanito Camilleri and Tom Melham Technical Report No. 265, University of Cambridge Computer Laboratory (August 1992). Inductively defined relations are among the basic mathematical tools of computer science. Examples include evaluation and computation relations in structural operational semantics, labelled transition relations in process algebra semantics, inductively-defined typing judgements, and proof systems in general. This paper describes a set of HOL theorem-proving tools for reasoning about such inductively defined relations. We also describe a suite of worked examples using these tools. Note that if I've already sent you a paper copy, the ftp version is identical so you won't want to bother. The HOL source code for the examples discussed in the paper is in contrib (HOL version 2.01). It is also available by anonymous ftp from ftp.cl.cam.ac.uk in the file /hvg/hol/rule-induction.tar.Z. Tom