Méthodes de filtrage équationnel et de preuve automatique de théorèmes / Jalel Mzali ; Sous la direction de Jean-Pierre Jouannaud

Date :

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Théorèmes -- Démonstration automatique

Filtres (informatique)

Jouannaud, Jean-Pierre (Directeur de thèse / thesis advisor)

Université Henri Poincaré Nancy 1. Faculté des sciences et techniques (Autre partenaire associé à la thèse / thesis associated third party)

Université de Nancy I (1970-2012) (Organisme de soutenance / degree-grantor)

Résumé / Abstract : 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