Return to search

Abstraction, partage de structure et retour arrière non aveugle dans la méthode de réduction matricielle en démonstration automatique de théorèmes

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

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00305297
Date30 November 1982
CreatorsCaferra, Ricardo
Source SetsCCSD theses-EN-ligne, France
LanguageFrench
Detected LanguageFrench
TypePhD thesis

Page generated in 0.0017 seconds