CM4

Question 1

Que signifie SMT ?

Answer 1

Satisfiability Modulo Theory

Question 2

Principes de la Déduction Modulo Théorie

Answer 2

• Transformer les axiomes en règles de réécriture
• Changer la recherche de preuve avec axiomes en calculs
• Éviter l’explosion combinatoiredans le recherche de preuve
• Réduire la taille des preuves en conservant uniquement les étapes significatives

Question 3

Principes de la Superdéduction

Answer 3

• Variant de la Déduction Modulo Théorie
• Les axiomes sont transformés en règles de réécriture puis traités à part avec les règles habituelles avant d’être utilisés

Question 4

Calcul des règles de Superdéduction avec les tableaux

Answer 4

• Entrée : les règles S des tableaux et l’axiome R : P → φ
• Écrire une règle de Superdéduction positive R et une règle de Superdéduction négative ¬R :
  
  • Initialiser la procédure avec φ
  • Appliquer les règles de S jusqu’à ce que plus aucune ne s’applique
  • Collecter les prémisses et la conclusion et remplace φ par P
• S’il y a des métavariables, ajouter une règle d’instanciations R_inst ou ¬R_inst