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 *G*_{F }of the language of *F* can be mechanically constructed from *F* such that *F* ⊬ *G*_{F }and *F* ⊬ ¬*G*_{F.}

*Kurt Gödel 1931*