Séance de cours
Cette séance de cours introduit un système de preuve pour les formules propositionnelles avec décision et simplification, en se concentrant sur la règle danalyse de cas et la résolution propositionnelle. L'instructeur explique la solidité du système de preuve et démontre des dérivations d'exemple. La séance de cours couvre les règles de simplification, les preuves d'insatisfaction, les conséquences de la solidité, l'exhaustivité de la réfutation et la résolution des clauses en tant que système de preuve. Il traite également de la forme conjonctive, des littéraux, des clauses et de la résolution en tant que transitivité dimplication. Des exercices sur l'utilisation de la résolution pour prouver la validité et l'insatisfaction de la formule sont inclus, ainsi que des concepts de résolution unitaire.