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; Fri, 16 Apr 1993 03:32:40 +0100 Received: by antares.mcs.anl.gov id AA13179 (5.65c/IDA-1.4.4 for qed-outgoing); Thu, 15 Apr 1993 21:27:38 -0500 Received: from linus.mitre.org by antares.mcs.anl.gov with SMTP id AA13171 (5.65c/IDA-1.4.4 for ); Thu, 15 Apr 1993 21:27:35 -0500 Received: from malabar.mitre.org by linus.mitre.org (5.61/RCF-4S) id AA28968; Thu, 15 Apr 93 22:27:31 -0400 Posted-Date: Thu, 15 Apr 93 22:27:28 -0400 Received: by malabar.mitre.org (5.61/RCF-4C) id AA02239; Thu, 15 Apr 93 22:27:28 -0400 Date: Thu, 15 Apr 93 22:27:28 -0400 From: jt@org.mitre.linus Message-Id: <9304160227.AA02239@malabar.mitre.org> To: qed@gov.anl.mcs Subject: little theories Cc: jt@org.mitre.linus, guttman@org.mitre.linus, farmer@org.mitre.linus Sender: qed-owner@gov.anl.mcs Precedence: bulk In reply to John Harrison's comment about `little theories', IMPS is indeed committed to a form of higher order logic. There are, however, a number of important differences between IMPS and HOL. For instance, the IMPS logic allows undefined terms and partial functions on sorts (which I do not believe HOL does.) But the main characteristic of IMPS is one of style. IMPS is designed to facilitate and encourage its users to develop mathematics as a network of theories interrelated by theory interpretations. These are the `little theories' mentioned by Josh Guttman earlier in the discussion. In our development of the IMPS theory library so far, we have aggressively exploited this strategy, we believe with some success. Javier Thayer