Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Tue, 9 Feb 1993 12:29:30 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06963; Tue, 9 Feb 93 04:16:07 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from iraun1.ira.uka.de by ted.cs.uidaho.edu (16.6/1.34) id AA06958; Tue, 9 Feb 93 04:15:56 -0800 Message-Id: <9302091215.AA06958@ted.cs.uidaho.edu> Received: from ira.uka.de by iraun1.ira.uka.de with SMTP (PP) id <28794-0@iraun1.ira.uka.de>; Tue, 9 Feb 1993 13:15:26 +0100 Date: Tue, 9 Feb 93 13:13:08 MET From: schneide To: info-hol@edu.uidaho.cs.ted Cc: schneide@de.uka.ira Subject: Basic Rules David Shepherd has said: > In fact HOL already has a "minimal set" of rules as many of the derived > rules while having an official definition using basic inference are > optimised by direct coding. It is the philosophy of the HOL system to have a (minimal) set of primitive rules. All other rules should be derived from this set of minimal rules, since the high level of security is based on this derivation of further rules. Hence, it cannot be the way to optimize the system by "implementing" further rules directly using "mk_thm". Another way of optimization could be to change the set of basic inference rules, which however would mean to reimplement a lot of the whole system. As some of the basic rules are redundant (e.g. REFL can be very easily implemented) they could be implemented as derived rules without large effort. Thus these basic rules could be neglected and other (redundant) rules which are more powerful and not easily derivable can be added as basic rules instead. In general, the set of basic rules has to be as small as possible, but it should also provide powerful rules, such that the whole system is reasonable fast.