Méthodes de schématisation pour la démonstration automatique - Université de Lorraine Access content directly
Theses Year : 1996

Schematization methods for theorem proving

Méthodes de schématisation pour la démonstration automatique

Ali Amaniss
  • Function : Author
  • PersonId : 787550
  • IdRef : 19094823X

Abstract

Not available
Ce travail se situe dans le cadre de la déduction automatique. Il traite d'une méthode, appelée la schématisation, utilisée pour remédier à des problèmes d'expressivité, d'efficacité et de divergence. La schématisation est un moyen de représentation finie d'ensembles infinis d'objets. Ceux-ci peuvent se retrouver dans différents domaines de l'informatique. Le but de notre travail est l'étude de cette méthode d'un point de vue théorique et pratique. D’un point de vue théorique, nous avons situé les classes de schématisation existantes dans la hiérarchie des langages d'arbres après les avoir comparé entre elles. Chose qui nous a permis de proposer des classes plus expressives que toutes les classes proposées jusqu'ici et qui sont intéressantes pour la déduction automatique. D’un point de vue pratique, nous avons proposé plusieurs algorithmes de manipulation de schématisations. Nous avons surtout introduit la notion de problème d'inclusion pour lequel nous avons donné un algorithme que nous avons applique à la généralisation inductive d'ensembles infinis de termes. Cet algorithme peut trouver d'autres applications dans le génie logiciel, la réécriture et le calcul des processus. Nous avons ensuite améliore l'algorithme classique de généralisation inductive dans ses cas d'échec en utilisant les I-termes puis les B-termes. Les algorithmes proposés peuvent être vus comme des procédures de construction automatique, respectivement, des I-termes et des B-termes.
No file

Dates and versions

tel-01747757 , version 1 (29-03-2018)

Identifiers

  • HAL Id : tel-01747757 , version 1

Intranet access

Cite

Ali Amaniss. Méthodes de schématisation pour la démonstration automatique. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 1996. Français. ⟨NNT : 1996NAN10092⟩. ⟨tel-01747757⟩
53 View
0 Download

Share

Gmail Facebook X LinkedIn More