From termination to the halting problem…

I am interested in automated deduction problems. Coming from the rewriting community, I have worked on rewriting termination proofs and more generally on proofs of rewriting properties, in the context of rule-based programming.

Putting now into perspective the inductive proof techniques I developed for equational theories, I am studying the provability problem into axiomatic theories. Moving to proof theory, I am investigating links between uncompleteness, undecidability and the halting problem.




My favourite theorem:

Assume F is a consistent axiomatic system which contains Robinson arithmetic. Then a sentence Gof the language of F can be mechanically constructed from F such that FGF  and F ⊬ ¬GF.

Kurt Gödel 1931