Chers tous,
le prochaine seminaire PPS est:
Jeudi 21 Janvier, 11h salle 3E91 –
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.
