Guillaume Burel (Max-Planck-Institut, Saarbrücken),

Des démonstrations plus simples via la déduction modulo

Quand on recherche des démonstrations dans une théorie donnée, on peut soit utiliser une axiomatisation, ce qui s'avère souvent peu efficace, soit des procédures spécifiques à cette théorie, comme le simplex pour l'arithmétique linéaire, ce qui n'est pas généralisable. Une troisième approche consiste à présenter la théorie de manière à retrouver les bonnes propriétés des systèmes de démonstration sans théorie. Ainsi, la déduction modulo consiste à présenter une théorie sous forme de règles de réécriture, puis d'appliquer les règles d'inférence d'un système usuel (par exemple la déduction naturelle ou le calcul des séquents) modulo la congruence engendrée par ce système de réécriture.

Nous présentons comment la déduction modulo permet de simplifier la recherche de démonstration en nous concentrant sur trois critères : premièrement, nous montrons comment transformer une théorie en système de réécriture tout en assurant l'élimination des coupures, ce qui se fait en complétant le système de réécriture à l'aide d'une procédure de type Knuth-Bendix ; deuxièmement, nous montrons comment obtenir des démonstrations plus courtes ; troisièmement, nous soulignons l'expressivité de la déduction modulo en encodant les systèmes de type purs fonctionnels au premier ordre modulo.

Ce dernier résultat permet d'envisager l'utilisation de la déduction modulo comme formalisme de base d'un environnement de démonstration combinant des démonstrations provenant de différents outils, certains étant directement basés sur la déduction modulo. En particulier, nous évoquerons également comment intégrer la déduction modulo dans un prouveur du premier ordre existant.