Date : 1992
Editeur / Publisher : [S.l.] : [s.n.] , 1992
Type : Livre / Book
Type : Thèse / ThesisLangue / Language : anglais / English
Résumé / Abstract : L'OBJECTIF DE CE TRAVAIL EST D'ACCROITRE L'EFFICACITE DES DEMONSTRATEURS DE THEOREMES GRACE A L'UTILISATION DES SYMETRIES. L'EVIDENCE THEORIQUE A MONTRE QU'IL EST PEU PROBABLE D'AVOIR UN DEMONSTRATEUR DE THEOREMES EFFICIENT, MEME POUR LE CALCUL PROPOSITIONNEL MAIS IL Y A DE L'ESPOIR QUE L'ON PUISSE DEVELOPPER DES DEMONSTRATEURS DE THEOREMES PRATIQUES POUR RESOUDRE UNE GRANDE CLASSE DE THEOREMES NATURELS. UNE GRANDE QUANTITE DE PROBLEMES PRESENTENT UNE CERTAINE STRUCTURE ET, BIEN QU'ILS PUISSENT ETRE FACILEMENT EXPRIMES, LES DEMONSTRATEURS DE THEOREMES FONT UN TRAVAIL REPETITIVE PUISQU'ILS NE PRENNENT PAS EN COMPTE CETTE STRUCTURE. LES SYMETRIES PEUVENT AIDER A EVITER DE FAIRE CE TRAVAIL NON-NECESSAIRE. KRISHNAMURTHY INTRODUISIT LE PRINCIPE DE SYMETRIE (EN FAIT, LE PRINCIPE DE SYMETRIE EST PLUS GENERAL) ET MONTRA LA FACON D'OBTENIR DES DEMONSTRATIONS COURTES SI L'ON UTILISE LA RESOLUTION AUGMENTEE DE CE PRINCIPE. NOUS AVONS UTILISE DEUX REPRESENTATIONS, UNE PREMIERE SOUS FORME DE CLAUSES ET UNE DEUXIEME OU NOUS AVONS ESSAYE D'ENONCER DES CONTRAINTES PLUS GENERALES (EN UTILISANT L'OPERATEUR DE CARDINALITE), ET AUSSI DE TROUVER LES SYMETRIES SANS DIFFICULTE. DANS LE MEME ORDRE D'IDEES, NOUS AVONS VOULU GENERALISER LE THEOREME DE PARTITION DU MODELE DE OXUSOFF ET RAUZY AVEC NOTRE DEUXIEME REPRESENTATION. NOUS EXPLIQUONS COMMENT LES SYMETRIES PEUVENT ETRE UTILISEES DANS L'EVALUATION SEMANTIQUE POUR ELAGUER L'ARBRE DE DEMONSTRATION D'UN PROBLEME. POUR CELA, NOUS ESSAYONS DE TROUVER, A CHAQUE NIVEAU DE L'ARBRE, LES SYMETRIES EXISTANTES ENTRE LES VARIABLES DU PROBLEME. LES SYMETRIES QUE NOUS TROUVERONS VONT AIDER A FAIRE UN RETOUR EN ARRIERE INTELLIGENT. DES EXEMPLES ET UNE SERIE DE RESULTATS SONT DONNES