Delivery-Date: 
Message-Id: <199304140006.AA02373@panther.cs.uidaho.edu>
To: qed@gov.anl.mcs
Cc: guttman@org.mitre.linus
Subject: Re: a multilingual approach
In-Reply-To: Your message of Tue, 13 Apr 93 17:10:38 -0400. <9304132110.AA10474@circe.mitre.org>
Date: Tue, 13 Apr 93 17:06:21 -0700
From: Phil Windley <windley@edu.uidaho.cs.panther>
Sender: qed-owner@gov.anl.mcs
Precedence: bulk


On Tue, 13 Apr 93 17:10:38 EDT, guttman@linus.mitre.org wrote:
+------------
| >  From: dam@ai.mit.edu (David McAllester)
| >  Subject: a multilingual approach
| 
|     [paragraph deleted]
| 
| >  Of course I can see no objection to collecting libraries of first
| >  order validities, I am just not sure how to use them.  Perhaps the
| >  IMPS notion of a "little theory" is relevant here.  A little theory is
| >  a signature, a set of axioms, and a set of consequences.  I probably
| >  could translate any IMPS theory directly into a set of Ontic theorems.
| 
| I think one of the advantages of the little theories version of the
| axiomatic method is this:  The little theory is a natural unit for
| interchanging results.  By organizing mathematics into a network of
| relatively fine theories, it lets us see exactly what assumptions we
| must discharge to justify using a particular group of theorems in a
| different framework.

Josh,

Just to clear up a few definitions, please review for us what you mean by
"little theories."  Are these the same as parametrized modules (PVS, EHDM,
OBJ3), abstract theories (HOL), and others whoch I'm not as familiar with,
but seem similar?

I suspect that one problem that we're all going to have is language; not
the object language of the theorem provers, but English.

--phil--

Phillip J. Windley, Asst. Professor   |  windley@cs.uidaho.edu
Laboratory for Applied Logic	      |  windley@panther.cs.uidaho.edu
Department of Computer Science        |
University of Idaho                   |  Phone: 208.885.6501  
Moscow, ID    83843                   |  Fax:   208.885.6645