Re: a multilingual approach
"Phil Windley" <windley@panther.cs.uidaho.edu>
Messageid: <199304140006.AA02373@panther.cs.uidaho.edu>
To: qed@mcs.anl.gov
Cc: guttman@linus.mitre.org
Subject: Re: a multilingual approach
Inreplyto: 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@panther.cs.uidaho.edu>
XMts: smtp
Sender: qedowner
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