L'étude des moyens de déductions pour entreprendre une construction assistée de programmes mène à la définition d'un système de déduction automatique capable :<br />- de traiter l'égalité d'une façon générale ;<br />- d'entreprendre la preuve de formules qui ne sont pas des théorèmes, d'étudier les causes d'échec ;<br />- d'effectuer un tri pour retirer d'un large ensemble d'informations, celles utiles à la preuve.<br /><br />Ces caractères ont pu être pris en compte dans le cadre d'un système général, de genre "déduction matérielle".<br />Certaines classes d'expression reçoivent toutefois un traitement particulier. Ainsi une méthode de codage permet de déterminer, sans simplification ni mise en forme normale, l'équivalence d'expressions numériques.
Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00293250 |
Date | 15 December 1980 |
Creators | Ouabdesselam, Farid |
Source Sets | CCSD theses-EN-ligne, France |
Language | French |
Detected Language | French |
Type | PhD thesis |
Page generated in 0.0013 seconds