Types, sorts and variable types
David McAllester (dam@ai.mit.edu)
Thu, 25 Aug 94 10:21:22 EDT
What will be important is to have a rich formal language which reflects
the everyday world of mathematics, where there is no concern with the
"ultimate" building blocks of mathematical concepts (as many suppose
sets and membership to be). Then one has to inquire what principles
are commonly appealed to in a given body of mathematics when it comes
to representing and checking proofs. The first part would be akin to
what some people have tried to do in AI with the representation of
common-sense knowledge.
Can I rephrase this as "definitions form the foundation"
and "definitions should be natural"?
David McAllester