Présentation et rapports d'activité

L'objectif du projet PROTHEO est la conception et la réalisation d'outils pour la spécification et la vérification de logiciels. Pour cela nous travaillons à la fois à un environnement permettant de prototyper de tels outils, à des démonstrateurs spécialisés sur les preuves par récurrence ou dans certaines théories équationnelles, et à des techniques de preuve spécifiques privilégiant l'utilisation des contraintes et des règles de réécriture.

Le projet comporte trois thèmes de recherche complémentaires : la résolution de contraintes, la mécanisation de la déduction par règles et stratégies, et la démonstration automatique de théorèmes. La complémentarité se traduit par exemple par le fait que nous utilisons les contraintes et les techniques de réécriture pour améliorer l'efficacité des démonstrateurs, et que nous formalisons les résolveurs de contraintes et les démonstrateurs à l'aide de règles contrôlées par des stratégies.

Contraintes

Mots clés : contraintes, résolution, satisfaisabilité, propagation, programmation entière, combinaison, collaboration de solveurs.

Nous étudions la satisfaisabilité et la résolution de systèmes de contraintes, aussi bien sur des domaines symboliques, comme les termes, que sur des domaines numériques, tels que les entiers naturels ou les réels. Nous cherchons à combiner des techniques de propagation de contraintes, de programmation entière, de déduction symbolique et à faire collaborer des résolveurs de contraintes ainsi que la combinaison de telles contraintes. Les procédures que nous obtenons sont fondamentales pour les processus de déduction avec contraintes développés dans le projet.

Réécriture et stratégies

Mots clés : réécriture, programmation fonctionnelle, programmation par règles, stratégie.

La réécriture est largement utilisée au sein du projet, d'une part comme technique essentielle dans les démonstrateurs et les résolveurs de contraintes que nous développons, d'autre part comme cadre logique pour spécifier et prototyper les outils que nous proposons. Dans ce type d'applications, la formalisation et l'étude des stratégies jouent un rôle important. Le calcul de réécriture nous donne le cadre général sur lequel fonder ces travaux.

Démonstration automatique

Mots clés : déduction, réécriture, récurrence, contraintes, paramodulation, résolution.

Nous développons des méthodes et des systèmes de recheche de preuve fondés sur la réécriture et la résolution de contraintes. Ces méthodes sont appliquées à la mécanisation du raisonnement en logique équationnelle, en logique du premier ordre et en logique d'ordre supérieure.

Les logiciels développés dans le projet nous servent à valider nos idées, à présenter nos travaux à la communauté scientifique, et à transférer nos connaissances vers des domaines d'applications.

Rapports d'activité: 2006 2005 2004 2003 2002 2001 2000 1999 1998 1997 1996 1995 1994