Practical Issues

We believe that Gödel machines should be built. Some people may be sceptical about the practicality of systematic proof technique testers as components of general problem solvers. But until a short while ago some people were also sceptical about the feasibility of universal program search methods. Recent work [38,40], however, already has shown that certain general methods can indeed offer certain practical advantages over traditional planning systems and reinforcement learners.

The well-developed field of automated theorem proving provides a rich set of alternatives for the initial Gödel machine set-up. Practical issues include:

1. Identify a particularly convenient hardware, presumably not based on Turing machines, but perhaps on recurrent neural network-like parallel systems, possibly emulated by software for a traditional personal computer.

2. Identify a particularly convenient formal language for describing the initial axioms and the set of possible proofs. For efficiency reasons this language should include a calculus for shortcuts and variables like the one informally used by mathematicians, who rarely use truly formal argumentation. Their papers not only abound with sentences like `It is easy to see ...'; they almost always also use informal sentences such as `Let $f$ denote a function ...' before they reuse the symbol $f$ in more formal statements. To facilitate a mimicry of elegant human proof techniques, the theorem-proving calculus should fully formalize temporary bindings of symbols traditionally introduced through text to symbols occurring in theorem sequences.

3. Identify a natural set of instructions for the programming language used by the initial proof searcher to construct proof techniques that calculate proofs--compare Section 2.2.1.

4. Identify potentially useful high-level theorems about the initial proof searcher's behavior and performance, to be added to the initial axioms, such that the proof searcher's initial task is facilitated because it does not have to prove these theorems from scratch.

Back to Goedel Machine Home Page