December 3, 2012: Thomas Sternagel completed his master studies

Thomas Sternagel successfully defended his master thesis on “Automatic Proofs in Equational Logic”.

In his thesis Thomas extended Knuth-Bendix completion such that it enables the generation of proof trees in equational logic. As a side effect this allows to certify completion proofs by means of trustable theorem provers. The main achievements of his thesis he presented at the 6th International Joint conference on automated deduction (IJCAR 2012) in Manchester.

Parts of Thomas’ research have been supported by the Hypo Förderungspreis 2011.

Starting in January 2013 Thomas will change his focus on constrained rewriting and collaborate in the joint FWF/JSPS project I 963-N15.