Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Mon, 8 Feb 1993 19:33:29 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA02429;
          Mon, 8 Feb 93 11:08:47 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA02424;
          Mon, 8 Feb 93 11:08:36 -0800
Received: from guillemot.cl.cam.ac.uk (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) to cl; Mon, 8 Feb 1993 19:07:40 +0000
To: schneide <schneide@de.uka.ira>
Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl
Subject: Re: Basic Rules
In-Reply-To: Your message of Mon, 25 Jan 93 10:23:40 +0700. <9301250928.AA27774@ted.cs.uidaho.edu>
Date: Mon, 08 Feb 93 19:07:35 +0000
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.414:08.02.93.19.07.43"@cl.cam.ac.uk>


schneide@de.uka.ira asks:

> ... [sketch of primitive basis of HOL omitted] 
> 
> Now my question: Is there any special reason for using
> these primitive operators and basic inference rules? And
> if not, wouldn't it be reasonable to have a minimal set 
> of basic rules? And if there are reasons for efficiency,
> why don't we take REWRITE_RULE as a basic rule of inference,
> since this rule is used very often.

I think part of the reason behind the particular set of inference
rules used in the primitive basis of HOL is that the system was
originally built on top of LCF, and it therefore inherited quite
a bit of its logical structure from that system. 

Tom