Return-Path: Delivery-Date: Received: from antares.mcs.anl.gov (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Tue, 13 Apr 1993 23:28:39 +0100 Received: by antares.mcs.anl.gov id AA18968 (5.65c/IDA-1.4.4 for qed-outgoing); Tue, 13 Apr 1993 16:10:54 -0500 Received: from linus.mitre.org by antares.mcs.anl.gov with SMTP id AA18961 (5.65c/IDA-1.4.4 for ); Tue, 13 Apr 1993 16:10:51 -0500 Received: from circe.mitre.org by linus.mitre.org (5.61/RCF-4S) id AA12832; Tue, 13 Apr 93 17:10:49 -0400 Posted-Date: Tue, 13 Apr 93 17:10:38 -0400 Received: by circe.mitre.org (5.61/RCF-4C) id AA10474; Tue, 13 Apr 93 17:10:40 -0400 Message-Id: <9304132110.AA10474@circe.mitre.org> To: dam@edu.mit.ai (David McAllester) Cc: qed@gov.anl.mcs 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@org.mitre.linus Sender: qed-owner@gov.anl.mcs 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