François Thiré

---

TP

0. Installer Coq
1. Introduction
2. More about proofs
3. Natural Deduction and reflection

Projet

Date de rendu: TODO.

• Projet
• Un simple DPLL en OCaml

Liens utiles

Coq

• Coq Manual
• Mathematical Components book
• SSreflect manual
• Software Foundations (Vol.1) (is not using the mathematical components library)

CDCL

• Comparaison entre DPLL et CDCL + quelques explications
• Déroulement de CDCL (avec backtracking) sur un exemple
• Amélioration de DPLL/CDCL avec des watchers