Abstract FR:

Implantation de différentes méthodes de démonstration automatique basées sur un algorithme de completion rapide appelé SKB et un algorithme de complétion qui privilégie la règle de simplification par rapport à celle de superposition, nous étudions cet algorithme et son implantation. Étude du filtrage pour la simplification et la réécriture des termes