Spécification et raisonnement logique à l'aide de schémas
De Ensiwiki.
Sommaire |
Spécification et raisonnement logique à l'aide de schémas
| Labo | LIG |
| Equipe | CAPP |
| Encadrants | Ricardo.Caferra@imag.fr,Vincent.Aravantinos@imag.fr,Nicolas.Peltier@imag.fr
|
Thème général
Le sujet proposé s'inscrit dans le cadre de l'inférence automatique ou assistée, dont l'objet est de développer des programmes informatiques dotés de capacités de raisonnement.
Parmi les formes de représentation des connaissances utilisées par les humains pour le raisonnement, les schémas ("skeletons") sont d'une grande utilité dans beaucoup de domaines. Ils constituent une façon économique de représenter l'information pertinente qui permet d'étendre le pouvoir d'expression des langages logiques existants, tout en conservant les propriétés utiles d'un point de vue de la mécanisation.
Compétences attendues
Dans la mesure où le sujet est suffisamment vaste pour pouvoir être adapté facilement, les pré-requis sont limités. En particulier, il n'est pas nécessaire de posséder des connaissances approfondies en logique. Tous les axes de travail proposés sont adaptés aux compétences d'un élève ingénieur.
Contexte du travail
L'étudiant travaillera au sein de l'équipe CAPP qui possède une expertise internationalement reconnue en déduction automatique (cf. http://capp.imag.fr/). Des possibilités de continuation en Master sont envisageables.
Sujet
Notre objectif est d'étendre les langages logiques usuels (tels que par exemple la logique propositionnelle ou le calcul des prédicats du 1er ordre) en considérant des itérations de formules indicées, e.g. p1 ou ... ou pn. La longueur de ces itérations dépend d'un (ou plusieurs) paramètres entiers (ici n), qui font partie intégrante du langage (et non du méta-langage comme c'est le cas habituellement). Si on fixe la valeur de ces paramètres, alors on obtient des formules logiques classiques (mais le nombre de valeurs possibles pour n étant infini, il est impossible de fixer n en pratique). Le but est de manipuler ces schémas de formules de manière symbolique, afin par exemple de prouver que les formules obtenues sont valides pour toute valeur de n.
Par exemple, en utilisant n'importe quel démonstrateur pour la logique propositionnelle, on peut facilement prouver que les formules suivantes sont contradictoires:
P1 et (P1 => P2) et non P2
P1 et (P1 => P2) et (P2 => P3) et non P3
P1 et (P1 => P2) et (P2 => P3) et (P3 => P4) et non P4
....
En utilisant les schémas, on peut prouver directement que: P1 et (ET pour 1 <= i <= n: Pi => Pi+1) et non Pn+1
est contradictoire (quelle que soit la valeur de n >= 0).
Résultats attendus
Nous proposons plusieurs axes de travail, distincts et complémentaires, qui seront à choisir et à préciser en fonction des objectifs et des préférences des étudiants concernés.
Expérimentations. On utilisera le logiciel RegSTAB (http://regstab.forge.ocamlcore.org/) développé par V. Aravantinos, qui implémente une procédure de preuve pour une classe particulière de schémas, appelés schémas réguliers. Etude de ``benchmarks, comparaison avec des SAT-solvers etc.
Implémentation. Il s'agit soit de contribuer à l'amélioration des performances du logiciel existant RegSTAB, soit d'implémenter une nouvelle approche, fondée sur une extension de la méthode de Davis et Putnam.
Etude de problèmes théoriques liés aux schémas et aux méthodes de preuves proposées: preuve de terminaison pour certaines sous-classes, complexité, indécidabilité etc.
Détection de cycles. Les procédures de preuve proposées ne terminent pas en général. Dans certains cas, le programme est capable de détecter lui-même qu'il revient à une situation identique (ou simplement similaire) à une configuration déja rencontrée. Un axe de recherche important consiste à essayer de définir de nouveaux algorithmes, plus performants et/ou plus généraux, permettant de détecter ces boucles et ainsi d'éviter la non terminaison. Ce travail peut être relié aux deux points précédents.
Extension à la logique du premier ordre.
