Recherche avancée sur les thèses de l'INSA de Lyon


Yim, Pascal. Résolution dans les systèmes formels abstraits : applications a la programmation en logique, aux systemes de reecriture et aux grammaires formelles.. Thèse. Villeurbanne : Institut National des Sciences Appliquées de Lyon, 1989. Disponible à la Bibliothèque Marie Curie.


Domaine(s) : D03 - Mathématiques
Indice Dewey : 511.3
Langue : Français
Mots-clés : INFORMATIQUE THEORIQUE, INTELLIGENCE ARTIFICIELLE, LOGIQUE FORMELLE, LOGIQUE MATHEMATIQUE, SYSTEME FORMEL, DEMONSTRATION AUTOMATIQUE, LANGAGE FORMEL, PROGRAMMATION LOGIQUE, GRAMMAIRE FORMELLE, REECRITURE, PROLOG, INFORMATIQUE



Directeur(s) de thèse : Boulaye, Guy
Etablissement de soutenance : INSA de Lyon
Etablissement de co-tutelle : LIA - Laboratoire d'Informatique Appliquée - Lyon
Laboratoire : Institut national des sciences appliquées de Lyon - Lyon, LIA - Laboratoire d'Informatique Appliquée - Lyon, Partenaire(s) de recherche : LIA - Laboratoire d'informatique et Automatique appliquées, Partenaire(s) de recherche : Service Thermique Aérospatiale, Cannes
Numéro national de thèse : 1989ISAL0041
Date de soutenance : 1989

Accès au format papier, disponiblités des exemplaires
Droits réservés, utilisation gratuite



Résumé français : Les mathématiciens utilisent habituellement les systèmes formels pour modéliser le raisonnement hypotético-déductif, en démontrant des théorèmes à partir d'axiomes par des chaînes de déductions successives. Des systèmes formels pour la géométrie, la logique, l'algèbre sont bien connus. Un but de la démonstration automatique consiste alors à trouver une procédure qui décide si une formule est un théorème ou non. Je donne une définition ensembliste des systèmes formels, utilisant une sémantique de point fixe. Cette définition de ce que j'appelle alors les systèmes formels abstraits permet une étude générale de la notion de preuve, basée sur l'opérateur fondamental de choix de Hilbert. Du point de vue informatique, l'essentiel est alors de réduire les choix possibles, de manière à obtenir une procédure la plus efficace possible, en conservant les propriétés de correction et complétude. La procédure obtenue appliquée à la programmation en logique donne la SLD-résolution habituelle. En réécriture, on retrouve très naturellement une forme de la sur-réduction. un algorithme d'analyse syntaxique dans les grammaires de Chomsky est obtenu facilement. Des applications moins classiques aux clauses de Horn gardées (logique parallèle), à la logique temporelle et à la logique contrainte sont également abordées.