Une technique d'abstraction et de partage de structure pour une methode de démonstration automatique non expérimentée jusqu'à présent est proposée. On donne aussi une généralisation de la règle d'inférence pour le cas propositionnel. Une preuve est séparée en plan + validation, ce qui correspond à séparer la partie purement déductive de l'algorithme d'unification. Cette séparation est utilisée pour détecter les ensembles responsables des échecs de validation pour un retour arrière non aveugle
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00305297 |
| Date | 30 November 1982 |
| Creators | Caferra, Ricardo |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.1006 seconds