| Titre : |
Un système de résolution de problèmes à tendance naturelle |
| Type de document : |
texte imprimé |
| Auteurs : |
Joubert, Michel, Auteur ; Colmerauer, Alain, Directeur de thèse |
| Editeur : |
Université D'Aix-Marseille |
| Année de publication : |
1974 |
| Importance : |
84 f. |
| Format : |
27 cm. |
| Note générale : |
Thèse d’État : Informatique : Marseille, Université D'Aix-Marseille : 1974
Annexe f. 85 - 98 . - Bibliogr. f. 99 - 100 |
| Langues : |
Français (fre) |
| Mots-clés : |
Informatique C-résolution Système sugiton questions-réponses résolution Tendance naturelle |
| Index. décimale : |
D000674 |
| Résumé : |
La première partie de la présente étude est consacrée à la définition et à la démonstration des propriétés d'une nouvelle règle d'inférence de clauses appelée c-résolution.
L'intérêt essentiel de cette règle d'inférence apparait dans le traitement de l'égalité en démonstration automatique.
L'axiomatisation classique de l'égalité en logique du premier ordre est étendue à la suite de la définition d'un symbole spécial Val dont l'utilité est de "marquer" les termes sur lesquels peuvent être opérées des substitutions définies par des égalités.
Il est prouvé que la démonstration automatique par c-résolution et factorisation est un système complet de réfutation en logique du premier ordre dans laquelle l'égalité est axiomatisée en fonction du symbole Val.
La seconde partie de cette étude est consacrée à la présentation d'un système de questions-réponses, entièrement basé sur les méthodes de démonstration automatique, avec lequel un utilisateur peu averti des concepts de démonstration automatique peut malgré tout converser dans un langage proche du français.
Ce système est opérationnel à l'heure actuelle et un certain nombre d'exemples de l'utilisation que l'on peut en faire sont exposés. |
Un système de résolution de problèmes à tendance naturelle [texte imprimé] / Joubert, Michel, Auteur ; Colmerauer, Alain, Directeur de thèse . - Université D'Aix-Marseille, 1974 . - 84 f. ; 27 cm. Thèse d’État : Informatique : Marseille, Université D'Aix-Marseille : 1974
Annexe f. 85 - 98 . - Bibliogr. f. 99 - 100 Langues : Français ( fre)
| Mots-clés : |
Informatique C-résolution Système sugiton questions-réponses résolution Tendance naturelle |
| Index. décimale : |
D000674 |
| Résumé : |
La première partie de la présente étude est consacrée à la définition et à la démonstration des propriétés d'une nouvelle règle d'inférence de clauses appelée c-résolution.
L'intérêt essentiel de cette règle d'inférence apparait dans le traitement de l'égalité en démonstration automatique.
L'axiomatisation classique de l'égalité en logique du premier ordre est étendue à la suite de la définition d'un symbole spécial Val dont l'utilité est de "marquer" les termes sur lesquels peuvent être opérées des substitutions définies par des égalités.
Il est prouvé que la démonstration automatique par c-résolution et factorisation est un système complet de réfutation en logique du premier ordre dans laquelle l'égalité est axiomatisée en fonction du symbole Val.
La seconde partie de cette étude est consacrée à la présentation d'un système de questions-réponses, entièrement basé sur les méthodes de démonstration automatique, avec lequel un utilisateur peu averti des concepts de démonstration automatique peut malgré tout converser dans un langage proche du français.
Ce système est opérationnel à l'heure actuelle et un certain nombre d'exemples de l'utilisation que l'on peut en faire sont exposés. |
|
Ajouter le résultat dans votre panier
Visionner les documents numériques
Faire une suggestion Affiner la rechercheUn système de résolution de problèmes à tendance naturelle (1974)
