Trying to translate a mathematical proof as it appears in a book into formal logic for verification is not so easy, even though most mathematicians would agree that it is always possible in theory. We need to make the theory concrete. We split the process into two parts. First, we will rewrite mathematical statements, theorems, and proof structures in an intermediate language we call h-code. h-code is a language suitable for all sorts of day-to-day mathematics that will come quite naturally to persons familiar with LISP. Of course, h-code leaves out the narrative structures found in text proofs (but replaces them with more code-like structures). The next step in the process is to translate h-code statements into symbolic logic. The process as a whole is analogous to the way the way PASCAL programs get compiled: first, PASCAL is translated into an intermediate language called p-code, and then the p-code is compiled to give the assembly language which can run on the computer.
Goals and requirements of h-code
In this section, we describe our progress in defining a useful, expressive, h-code. The development process is closely related to our work on parsing tools (our parser's object language is h-code) and formal mathematics (h-code needs to be translated to a lower-level language for proof-checking). Eventually our AI system should implement heuristics that apply to h-code structures for conjecture-generation and other purposes.
Somewhat in-depth discussion about hcode-related matters.
Here we describe (or exhibit) LISP code relevant to this sub-project. See also HDM CVS.
Back to HDM.