# Re: a multilingual approach

guttman@linus.mitre.org
Message-id: <9304132110.AA10474@circe.mitre.org>
To: dam@ai.mit.edu (David McAllester)
Cc: qed@mcs.anl.gov
Subject: Re: a multilingual approach
In-reply-to: Your message of "Tue, 13 Apr 93 15:35:55 EDT."
<9304131935.AA00351@spock>
X-Postal-Address: MITRE, Mail Stop A156 \\ 202 Burlington Rd. \\ Bedford, MA 01730
X-Telephone-Number: 617 271 2654; Fax 617 271 3816
Date: Tue, 13 Apr 93 17:10:38 -0400
From: guttman@linus.mitre.org
Sender: qed-owner
Precedence: bulk

> 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