Ammon, K., An automatic proof of G~lel's incompleteness theorem (Research Note), Artificial Intelligence 61 (1993) 291-306.
The SHUNYATA program contains heuristics which are related to reasoning processes of mathematicians and guide the search for a proof. For example, a heuristic applies the method of reductio ad absurdum to prove the negation of a proposition. Another heuristic generates formulas and sets which form the central "ideas" of significant proofs. Some heuristics control the application of other heuristics, for example, by time limits which interrupt a heuristic if it achieves no result. The architecture and the mode of operation of SHUNYATA are illustrated in detail by SHUNYATA's proof of G6del's incompleteness theorem which says that every formal number theory contains an undecidable formula, i.e., neither the formula nor its negation are provable in the theory. In this proof, SHUNYATA constructed several closed formulas on the basis of elementary rules for the formation of formulas and proved that one of these formulas is undecidable. Further experiments with a learning procedure suggest that an automatic construction of SHUNYATA's heuristics on the basis of a universal set of elementary functions is feasible.