What are some implications of Gödel's theorems on AI research? Note: My experience with Gödel's theorem is quite limited: I have read Gödel Escher Bach; skimmed the 1st half of Introduction to Godel's Theorem (by Peter Smith); and some random stuff here and there on the internet. That is, I only have a vague high level understanding of the theory. 

In my humble opinion, Gödel's incompleteness theorem (and its many related Theorems, such as the Halting problem, and Löbs Theorem) are among the most important theoretical discoveries. 

However, its a bit disappointing to observe that there aren't that many (at least to my knowledge) theoretical applications of the theorems, probably in part due to 1. the obtuse nature of the proof 2. the strong philosophical implications people aren't willing to easily commit towards.

Despite that, there are still some attempts to apply the theorems in a philosophy of mind / AI context. Off the top of my head:


The Lucas-Penrose Argument: which argues that the mind is not implemented on a formal system (as in computer). (Not a very rigour proof however) 
Apparently, some of the research at MIRI uses Löbs Thereom, though the only example I know of is Löbian agent cooperation.


These are all really cool, but are there some more examples? Especially ones that are actually seriously considered by the academic community.

See also What are the philosophical implications of Gödel's First Incompleteness Theorem?
Definitely there are a lot of implications for AI, including:


Inference with first-order-logic is semi-decidable. This is a big disappointment for all the folks that wanted to use logic as a primary AI tool.
Basic equivalence of two first-order logic statements is undecidable, which has implications for knowledge-based systems and databases. For example, optimisation of database queries is an undecidable problem because of this.
Equivalence of two context-free grammars is undecidable, which is a problem for formal linguistic approach toward language processing
When doing planning in AI, just finding a feasible plan is undecidable for some planning languages that are needed in practice.
When doing automatic program generation - we are faced with a bunch of decidability results, since any reasonable programming language is as powerful as a Turing machine.
Finally, all non-trivial questions about an expressive computing paradigm, such as Perti nets or cellular automata, are undecidable.