Mécanisation de la recherche de preuves et de programmes en arithmétique fonctionnelle du second ordre - Université de Lorraine Access content directly
Theses Year : 1995

Mechanization of proof search for program synthesis in the second order functional arithmetic

Mécanisation de la recherche de preuves et de programmes en arithmétique fonctionnelle du second ordre

Odile Hermann
  • Function : Author
  • PersonId : 787714
  • IdRef : 191652008

Abstract

Not available
Ce travail a pour propos la synthèse de programmes à partir de preuves constructives dans un cadre logique spécifique: l'arithmétique fonctionnelle du second ordre. Une première étape consiste à proposer une transcription du système de règles initial exprime en déduction naturelle, en un système de séquents plus adapte au traitement automatique du développement de preuves. Pour mécaniser la recherche de preuves, nous définissons un ensemble de tactiques que nous prouvons correctes vis-à-vis du cadre logique de référence de façon à garantir l'adéquation du système de preuves obtenu. Parmi ces tactiques, nous nous concentrons sur les plans de preuve, tactiques particulières capables de développer complètement une preuve ou une classe de preuves. La partie centrale de notre travail consiste en une étude des mécanismes d'induction dont la mise en œuvre est nécessaire pour l'obtention de programmes définis récursivement. Nous montrons des liens entre forme d'induction, spécification du programme, définition des types de données, et réussite de la construction de la preuve. Pour tirer profit de cette étude, nous proposons une procédure de choix d'induction et un plan de preuve générique qui permet d'obtenir des programmes aussi variés que la fonction d'Ackermann, la fonction Fibonacci ou le tri d'une liste par arbre binaire. Ces travaux ont fait l'objet de l'implantation d'un système baptise SKIL (Synthesizing Knowledge in Intuitionistic Logic)
No file

Dates and versions

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

Identifiers

  • HAL Id : tel-01747993 , version 1

Intranet access

Cite

Odile Hermann. Mécanisation de la recherche de preuves et de programmes en arithmétique fonctionnelle du second ordre. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 1995. Français. ⟨NNT : 1995NAN10054⟩. ⟨tel-01747993⟩
22 View
0 Download

Share

Gmail Facebook X LinkedIn More