E-Learning Project accepted (May 23, 2011)

Proving if two objects are equivalent (modulo some axioms) is the main aim of the new eLearning project led by Dr. Harald Zankl.

In an earlier project the Knuth-Bendix completion procedure has been visualized for this purpose. In this follow-up project we focus on the generation of proof trees that prove two objects equivalent (modulo some axioms). In the course of this project a tool will be developed which helps students to find proof trees.