Introduction à la logique

René David, Karim Nour, Christophe Raffalli (DNR)

Utilisée dans les 6 développements suivants :

Algorithme d'unification
Constructivité de la logique intuitionniste
Décidabilité de l'arithmétique de Presburger
Théorie des ordres denses
Une involution est bijective
LK (LJ) ⇒ NK (NJ)

Utilisée dans les 5 leçons suivantes :

917 (2016) Logique du premier ordre : syntaxe et sémantique.
918 (2021) Systèmes formels de preuve en logique du premier ordre. Exemples.
924 (2021) Théories et modèles en logique du premier ordre. Exemples.
919 (2017) Unification : algorithmes et applications.
921 (2021) Algorithmes de recherche et structures de données associées.

Utilisée dans les 8 versions de développements suivants :


Utilisée dans les 8 versions de leçons suivantes :