La technique du renommage, appliquée exhaustivement, permet d'obtenir une forme clausale polynomiale. Nous choisissons de l'appliquer partiellement, de façon a minimiser certains criteres syntaxiques, principalement le nombre de clauses, tout en conservant une complexité polynomiale. Nous montrons qu'un algorithme efficace permet d'obtenir le nombre optimal de clauses sur les formules linéaires. Enfin, nous étudions l'influence de ces transformations sur les réfutations par la methode de resolution, autant théoriquement expérimentalement
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00339269 |
| Date | 21 January 1991 |
| Creators | Boy De La Tour, Thierry |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.002 seconds