translation into a standard language
John McCarthy (jmc@sail.Stanford.EDU)
Thu, 11 Aug 94 16:47:19 -0700
This is inspired by Peter Andrews's message. He discusses translating
theorems and proofs from one system to another. I think that
translating theorems is needed and translating proofs, which is much
harder, can be dispensed with. I suspect that set theory can serve as
a universal language. Every system can have a translator into set
theory for its theorems. However, most likely only a subset of set
theory will be translatable into systems like Boyer-Moore in any
automatic way. The translator for Boyer-Moore should recognize what
it can translate. The set theory itself used as a universal language
need not have a prover of its own and quite likely will not be the
same as the language of someone's set theory based prover.