Étude et instances de systèmes de preuves ordonnées - École Jeunes Chercheurs en Programmation

Étude et instances de systèmes de preuves ordonnéesÉcole Jeunes Chercheurs en ProgrammationGuillaume BurelLORIA – Université Henri PoincaréEncadrant : Claude Kirchnerjuin 2006Guillaume Burel (LORIA/UHP) Systèmes de preuves ordonnées juin 2006 1 / 7Différentes représentations des preuves mais une notion commune : certainespreuves sont «meilleures» que d’autres : preuves sans coupures, preuves parréécriture, preuves qui appliquent la résolution sur les grands atomes enpremierCadre des systèmes canoniques abstraits (SCA) introduit par N.Dershowitz etC. Kirchner : la notion de bonne preuve est traduite par un ordre sur lespreuvesNotion de complétion abstraite qui permet de retrouver un système ayant lesbonnes propriétés; ici on va l’appliquer à la déduction modulo pour recouvrerl’élimination des coupuresIntroductionDémonstration automatique et interactive : de nombreux formalismeslogiques : séquents, preuves équationnelles, formes clausales...Guillaume Burel (LORIA/UHP) Systèmes de preuves ordonnées juin 2006 2 / 7preuves sans coupures, preuves parréécriture, preuves qui appliquent la résolution sur les grands atomes enpremierCadre des systèmes canoniques abstraits (SCA) introduit par N.Dershowitz etC. Kirchner : la notion de bonne preuve est traduite par un ordre sur lespreuvesNotion de complétion abstraite qui permet de retrouver un système ayant lesbonnes propriétés; ici on va l’appliquer à la déduction modulo pour recouvrerl’élimination des ...