ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne
Autres revues >>

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 22/RSTI1 - 2003  - pp.190-202
TITRE
Extraction de programmes à partir de spécifications en logique existentielle du second ordre par compilation de connaissances

RÉSUMÉ
Nous étudions la compilation de problèmes exprimés en logique existentielle de second ordre, un langage expressif dans lequel une large classe de problèmes combinatoires peut être exprimée. On entend par "compilation" le fait de rendre explicites certaines règles de déduction qui sont implicites dans la formulation initiale du problème. Le problème initial est ainsi traduit dans une forme soluble par des méthodes de raisonnement simples. Notre approche est une adaptation de techniques de compilation de connaissances, qui ont récemment été proposées pour accélérer les déductions dans les bases de connaissances. Nous l'illustrons sur des problèmes simples issus de la théorie des graphes. Nous montrons que certains algorithmes classiques peuvent être extraits automatiquement de la formulation logique du problème. La technique de compilation est nécessairement incomplète et son succès repose sur une propriété de localité. Nous proposons un test à base de compilation de connaissances permettant de tester si cette propriété est vérifiée.


ABSTRACT
We study the compilation of problems specified in second-order existential logic, an expressive language in which a wide class of combinatorial problems is known to be expressible. Compilation is understood as the task of making explicit some deduction rules which are implicit in the statement of the problem, in order to make it solvable by simple reasoning algorithms. Our approach is an adaptation of some knowledge-compilation techniques used to speed-up deduction in knowledge bases. We illustrate it on simple problems from graph-theory, for which we show that algorithms can be automatically derived from their logical statement. The technique is necessarily incomplete and relies on a locality property which must hold for the compilation to be successful. We provide an algorithm based on knowledge-compilation to check this property.


AUTEUR(S)


MOTS-CLÉS
SAT, logique existentielle de second ordre, compilation de connaissances.

KEYWORDS
SAT, existential second-order logic, knowledge-compilation.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 12.5 €
• Non abonné : 25.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (222 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier