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 GF of the language of F can be mechanically constructed from F such that F ⊬ GF and F ⊬ ¬GF.
Kurt Gödel 1931
