HomePage RecentChanges

(redirected from hcode)

h-code

Introduction

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.

Advantages of h-code

Goals and requirements of h-code

Progress in h-code Development

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.

an early sketch
showing the what the language should look like in very simple examples
Version Zero
the (evolving) spec for the basic language
Hcode libraries
(evolving) "standard" libraries to test out the evolving spec

general hcode discussion

hcode topics

Somewhat in-depth discussion about hcode-related matters.

hcode coding

Here we describe (or exhibit) LISP code relevant to this sub-project. See also HDM CVS.

miscellaneous


Back to HDM.