From owner-qed Wed Aug 24 19:06:44 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id TAA01860 for qed-out; Wed, 24 Aug 1994 19:06:01 -0500 Received: from oracorp.com (scylla.oracorp.com [192.76.175.102]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id TAA01855 for ; Wed, 24 Aug 1994 19:05:54 -0500 From: hoove@oracorp.com Received: from euterpe.oracorp.com by oracorp.com (4.1/2.1-ORA Corporation) id AA03048; Wed, 24 Aug 94 20:04:05 EDT Date: Wed, 24 Aug 94 20:04:04 EDT Received: by euterpe.oracorp.com (4.1/1.3-ORA Corporation) id AA01946; Wed, 24 Aug 94 20:04:04 EDT Message-Id: <9408250004.AA01946@euterpe.oracorp.com> To: qed@mcs.anl.gov Subject: Re: Types and sorts Sender: owner-qed@mcs.anl.gov Precedence: bulk farmer@linus.mitre.org writes: There is a distinction between "types" and "sorts" in the IMPS logic (officially named LUTINS) that might be helpful to the recent discussion about type theory vs. set theory. etc. I wonder if he would be willing to compare the type theory of IMPS to that of PVS. In PVS, types are closed under subtypes (any predicate defines a subtype of a type) so it appears that PVS-type = IMPS-(type or sort) I prefer PVS because I don't see the advantage of distinguishing types and sorts. Am I missing something? Doug Hoover hoove@oracorp.com