DEMONSTRATION AUTOMATIQUE DANS LES THEORIES DE HORN
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'...
Wedi'i Gadw mewn:
| Prif Awdur: | |
|---|---|
| Awduron Eraill: | |
| Fformat: | Thèse et Mémoire papier |
| Iaith: | Français |
| Cyhoeddwyd: |
[S.l.] :
[s.n.]
1991.
|
| Pynciau: | |
| Nodyn: |
1991ORLE2005 |
| Autres localisations: | Voir dans le Sudoc |
| Variante du titre: | THEOREM-PROVING IN HORN THEORIES |
| LEADER | 02411nam a22002537a 4500 | ||
|---|---|---|---|
| 001 | 196876 | ||
| 008 | 990313s1991 xxe ||| |||| 00| 0 fre d | ||
| 009 | PPN044188811 | ||
| 041 | 0 | |a fre |b fre | |
| 084 | |a 001.D.02.C | ||
| 084 | |a 620 | ||
| 100 | 1 | |a Andrianarivelo, Nirina, |d 19..-...., |c chercheuse en informatique. | |
| 240 | 1 | 0 | |a THEOREM-PROVING IN HORN THEORIES |
| 245 | 1 | 0 | |a DEMONSTRATION AUTOMATIQUE DANS LES THEORIES DE HORN |c NIRINA ANDRIANARIVELO ; SOUS LA DIRECTION DE SIVA ANANTHARAMAN. |
| 260 | |a [S.l.] : |b [s.n.], |c 1991. | ||
| 500 | |a 1991ORLE2005 | ||
| 502 | |a Thèse Doctorat. Sciences appliquées. Orléans. 1991 | ||
| 504 | |a 58 REF | ||
| 520 | |a 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 | ||
| 650 | |a Thèses et écrits académiques | ||
| 700 | 1 | |a Anantharaman, Siva, |d 19..-...., |c professeur en informatique. |4 ths | |
| 710 | 2 | |a Université d'Orléans. |4 dgg | |
| 997 | |0 196876 |1 Thèse et Mémoire papier |a Ressource papier |c 0/Orléans/ |c 1/Orléans/BU Sciences, Technologies, STAPS/ |z Orléans, BU Sciences, Technologies, STAPS, TS 19-1991-5 |z Orléans, BU Sciences, Technologies, STAPS, TS 19-1991-5 b | ||
| 999 | |5 452342104:056704194 |a ORLEANS | ||