Mes activités portent sur divers aspects de la Démonstration Automatique:

• transformation sous forme clausale
• analogie entre preuves
• symétries dans les preuves
• unification dans les théories permutatives
• généralisation de preuves