little theories

• Mail folder: QED
• Next message: guttman@linus.mitre.org: "Re: "Little Theories" and the base logic "
• Previous message: : ""

Date: Thu, 15 Apr 93 22:27:28 -0400
From: jt@linus.mitre.org
Message-id: <9304160227.AA02239@malabar.mitre.org>
To: qed@mcs.anl.gov
Subject: little theories
Cc: jt@linus.mitre.org, guttman@linus.mitre.org, farmer@linus.mitre.org
Sender: qed-owner
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