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 be individuals, like other individuals, with some being
integers, some real, and so on.
Any references to results of existing efforts to explore the potential
and/or issues raised by such arrangements would be much appreciated.
A significant part of my own interest in this approach is related to
usability by non-specialists, and in that sense style might be more an
issue than ultimate expressive power. Ideally such a system would also
support a relatively flexible and rich system of "types", without the need
to bring in the conceptual complexity of dependent types, and their
accompanying notations.
Best regards and thanks in advance,
Cris
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
