On 27/01/18 23:04, Cris Perdue wrote:
> Well no. If a person has neither special preparation nor interest, I would
> not wish to bother them.
If you are willing to take a request from me, please do not use “they”
as singular. In English, “he” is the canonical generic singular.
Although “they” has
Dear Mario,
Thank you for your thoughtful, detailed, and even rather delightful
response. I'll respond to your email in a block here, in hopes of better
continuity in my reply.
Yes, I really am interested in extending a simple system of higher-order
logic with new predicates for new "datatypes"
On 22/01/18 18:35, Cris Perdue wrote:
> Are any of you readers of this list aware of investigations or
> implementations of logics that, like the HOL family of provers, are based
> on the simple theory of types, but which support introduction of new types
> through new predicates rather than new
t;
>
>
>
> *From: *Cris Perdue <c...@perdues.com>
> *Date: *Tuesday, 23 January 2018 at 11:36
> *To: *hol-info <hol-info@lists.sourceforge.net>
> *Subject: *[Hol-info] Inquiry: Introducing new types as predicates
>
>
>
> Are any of you readers
offered by PVS?
Michael
From: Cris Perdue <c...@perdues.com>
Date: Tuesday, 23 January 2018 at 11:36
To: hol-info <hol-info@lists.sourceforge.net>
Subject: [Hol-info] Inquiry: Introducing new types as predicates
Are any of you readers of this list aware of investigations or imp
Are any of you readers of this list aware of investigations or
implementations of logics that, like the HOL family of provers, are based
on the simple theory of types, but which support introduction of new types
through new predicates rather than new type constants? Presumably numbers
then could
