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; Fri, 9 Apr 1993 09:44:16 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08596;
          Fri, 9 Apr 93 01:27:45 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA08589;
          Fri, 9 Apr 93 01:27:26 -0700
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA22336;
          Fri, 9 Apr 93 01:27:14 -0700
Message-Id: <9304090827.AA22336@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: A few Q's
Date: Fri, 09 Apr 93 01:27:12 PDT
From: chou@edu.ucla.cs

Dear netters,

I have a few questions.  I'd appreciate your comments.

(1) Who was the first person who used a general logical formalism
    (eg, HOL) to embed a specialized logic (eg, temporal logic or
    Hoare logic)?  


(2) Is there any embedding work using other general logical formalisms
    such as ZFC or Nuprl?  (By the way, is there a good theorem prover
    for ZFC?)

(3) What is your view about general versus specialized logics?
    For the former, I can see several advantages: higher security
    (if the base logic can be trusted and only definitional extensions
    are used), flexibility of mixing specialized reasoning with
    general mathematical reasoning, and no need to worry about the
    completeness of axioms and rules since new ones can always be
    proved and added when necessary.  What are the latter's advantages?


- Ching Tsun