Qu’est-ce qu’une preuve formelle?

Cette séance de cours introduit le concept d'un système de preuve formel, le définissant comme un ensemble de formules logiques avec des étapes d'inférence. Il explique la structure dune preuve dans un système de preuve et comment les preuves peuvent être considérées comme des graphiques acycliques dirigés. Un exemple de système de logique propositionnelle est présenté, ainsi que des exercices pour dessiner des DAG représentant des preuves. La séance de cours couvre la solidité dun système de preuve, les dérivations dhypothèses, les conséquences sémantiques, et limportance des règles dinférence saines pour assurer la validité des formules.