a multilingual approach

• Mail folder: QED
• Next message: guttman@linus.mitre.org: "Re: a multilingual approach "
• Previous message: David McAllester: "the base logic"
• Reply: guttman@linus.mitre.org: "Re: a multilingual approach "

From: dam@ai.mit.edu (David McAllester)
Date: Tue, 13 Apr 93 15:35:55 EDT
Message-id: <9304131935.AA00351@spock>
To: qed@mcs.anl.gov
Subject: a multilingual approach
Sender: qed-owner
Precedence: bulk

I should have said that theorems from any group that I did not mention
would, of course, be nice to also have in a repository.  I am not
quite sure how I would use the theorems proved by resolution provers
unless they were translated into some foundational language.  I'm not
sure how to use first order validities.  What kind of mathematical
objects does a particular validity talk about?  Figuring this out
automatically from the statement of the validity seems difficult.  I
would like libraries to contain statements like "every finite Abelion
group is isomorphic to a product of cyclic subgoups".  How would this
be phrased as a first order validity?  Given appropriate higher order
definitions this theorem can be formalized more or less as stated.

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.
(Please let me know if I have misrepresented IMPS).

	David McAllester