Date : 1991
Editeur / Publisher : [S.l.] : [s.n.] , 1991
Type : Livre / Book
Type : Thèse / ThesisLangue / Language : français / French
Résumé / Abstract : NOTRE OBJECTIF EST DE PRESENTER UN SYSTEME D'INFERENCE ASSEZ EFFICACE POUR LA DEMONSTRATION AUTOMATIQUE DANS LES THEORIES DE HORN AVEC EGALITE. NOTRE APPROCHE ADOPTE UNE STRATEGIE UNITAIRE ET ELLE EST PROUVEE CORRECTE ET COMPLETE POUR LES THEOREMES DEDUCTIFS SANS POUR AUTANT SUPPOSER QUE L'ORDRE SOIT UN ORDRE DE SIMPLIFICATION COMPLET. LA PREMIERE PARTIE DE CE TRAVAIL EST CONSACRE A DES AMELIORATIONS NECESSAIRES DE L'UKB DE BACHMAIR (1987). NOUS LUI AJOUTONS LES NOUVEAUTES SUIVANTES: UNE REGLE D'INFERENCE DITE TRANSFORMATION DES INEGALITES; DES CRITERES DE SUPPRESSION DE REGLES, QUANTITATIFS ET ORIENTES PAR LE THEOREME A PROUVER; ET DES STRATEGIES DE CHOIX DE REGLES, BASEES SUR UNE NOTION QUANTITATIVE ET ORIENTEES PAR LE THEOREME A REFUTER. DANS LA SECONDE PARTIE DU TRAVAIL, NOUS PROPOSONS UNE STRATEGIE UNITAIRE POUR PROUVER UN THEOREME DEDUCTIF DANS LES THEORIES DE HORN. ELLE NE CALCULE LES PAIRES CRITIQUES QU'ENTRE REGLES STANDARDS (ELLE EST DONC PLUS QU'UNITAIRES), ET N'UTILISE AUCUNE NOTION DE REDUCTION CONDITIONNELLE (CONTEXTUELLE) ET LES SUPERPOSITION-INSTANCES NE SONT FAITES QU'ENTRE REGLES STANDARDS ET REGLES CONDITIONNELLES. DANS LA DERNIERE PARTIE, NOUS PRESENTONS LE LOGICIEL SBR3 QUI A PU INCORPORER LA PLUPART DES AMELIORATIONS PROPOSEES DANS LA PREMIERE PARTIE DE CETTE THESE