Logique et démonstration automatique - Introduction à la logique propositionnelle et à la logique du premier ordre /// (Version Complétée de l'UE UGA INF402 Année 2020/2021)

I Logique propositionnelle
	1 Logique propositionnelle
		1.1 Syntaxe
			1.1.1 Formules strictes
			1.1.2 Formules à priorité
		1.2 Sens des formules
			1.2.1 Sens des connecteurs
			1.2.2 Valeur d\'une formule
			1.2.3 Définitions et notions élémentaires de logique
			1.2.4 Compacité
			1.2.5 Équivalences remarquables
		1.3 Substitution et remplacement
			1.3.1 Substitution
			1.3.2 Remplacement
		1.4 Formes Normales
			1.4.1 Transformation en forme normale
			1.4.2 Transformation en forme normale disjonctive (somme de monômes)
			1.4.3 Transformation en forme normale conjonctive (produit de clauses)
		1.5 Algèbre de Boole
			1.5.1 Définition et notations
			1.5.2 Propriétés
			1.5.3 Dualité
		1.6 Fonctions booléennes
			1.6.1 Fonctions booléennes et somme de monômes
			1.6.2 Fonctions booléennes et produit de clauses
		1.7 L\'outil BDDC
		1.8 Exercices
	2 Résolution propositionnelle
		2.1 Résolution
			2.1.1 Définitions
			2.1.2 Cohérence
			2.1.3 Complétude pour la réfutation
			2.1.4 Réduction d\'un ensemble de clauses
			2.1.5 Clauses minimales pour la déduction
			2.1.6 Clauses minimales pour la conséquence
		2.2 Stratégie complète
			2.2.1 Algorithme de la stratégie complète
			2.2.2 Arrêt de l\'algorithme
			2.2.3 Le résultat de l\'algorithme est équivalent à l\'ensemble initial de clauses
			2.2.4 Le résultat de l\'algorithme est l\'ensemble des clauses minimales pour la déduction de l\'ensemble initial de clauses
		2.3 Algorithme de Davis-Putnam-Logemann-Loveland
			2.3.1 Suppression des clauses contenant des littéraux isolés
			2.3.2 Résolution unitaire
			2.3.3 Suppression des clauses valides
			2.3.4 L\'algorithme
			2.3.5 Solveurs SAT
				2.3.5.1 Heuristique de branchement
				2.3.5.2 Ajout de clauses
				2.3.5.3 Analyse des conflits et retour-arrière non chronologique
				2.3.5.4 Apprentissage
				2.3.5.5 Redémarrage
				2.3.5.6 Structures de données paresseuses
		2.4 Exercices
	3 Déduction Naturelle
		3.1 Système formel de la déduction naturelle
			3.1.1 Règles de conjonction
			3.1.2 Règles de disjonction
			3.1.3 Règles de l\'implication
			3.1.4 Deux règles spéciales
			3.1.5 Preuves en déduction naturelle
				3.1.5.1 Brouillon de preuve
				3.1.5.2 Contexte des lignes d\'un brouillon de preuve
				3.1.5.3 Preuves
		3.2 Tactiques de preuve
		3.3 Cohérence de la déduction naturelle
		3.4 Complétude de la déduction naturelle
		3.5 Outils
			3.5.1 Logiciel de construction automatique de preuves
			3.5.2 Dessiner des arbres de preuves
		3.6 Exercices
II Logique du premier ordre
	4 Logique du premier ordre
		4.1 Syntaxe
			4.1.1 Formules strictes
			4.1.2 Formules à priorité
		4.2 Être libre ou lié
			4.2.1 Occurrences libres et liées
			4.2.2 Variables libres et liées
		4.3 Sens des formules
			4.3.1 Déclaration de symbole
			4.3.2 Signature
			4.3.3 Interprétation
			4.3.4 Sens des formules
				4.3.4.1 Sens des termes sur une signature
				4.3.4.2 Sens des formules atomiques sur une signature
				4.3.4.3 Sens des formules sur une signature
			4.3.5 Modèle, validité, conséquence, équivalence
			4.3.6 Instanciation
			4.3.7 Interprétation finie
				4.3.7.1 Les entiers et leurs représentations
				4.3.7.2 Expansion d\'une formule
				4.3.7.3 Interprétation et assignation propositionnelle
				4.3.7.4 Recherche d\'un modèle fini d\'une formule fermée
			4.3.8 Substitution et remplacement
		4.4 Équivalences remarquables
			4.4.1 Relation entre  et
			4.4.2 Déplacement des quantificateurs
			4.4.3 Changement de variables liées
		4.5 Exercices
	5 Base de la démonstration automatique
		5.1 Méthode de Herbrand
			5.1.1 Domaine et base de Herbrand
			5.1.2 Interprétation de Herbrand
			5.1.3 Théorème de Herbrand
		5.2 Skolémisation
			5.2.1 Algorithme de skolémisation d\'une formule
				5.2.1.1 Transformation en formule normale
				5.2.1.2 Transformation en formule propre
				5.2.1.3 Élimination des quantificateurs existentiels
				5.2.1.4 Transformation en fermeture universelle
			5.2.2 Propriétés de la forme de Skolem
			5.2.3 Forme clausale
		5.3 Unification
			5.3.1 Unificateur
			5.3.2 Algorithme d\'unification
				5.3.2.1 Les règles de l\'algorithme
				5.3.2.2 Correction de l\'algorithme
				5.3.2.3 Terminaison de l\'algorithme
		5.4 Résolution au premier ordre
			5.4.1 Trois règles pour la résolution
				5.4.1.1 Factorisation
				5.4.1.2 Copie d\'une clause
				5.4.1.3 Résolution binaire
				5.4.1.4 Preuve par factorisation, copie et résolution binaire
			5.4.2 Cohérence de la résolution
			5.4.3 Complétude de la résolution
		5.5 Outil logiciel
		5.6 Exercices
	6 Déduction naturelle au premier ordre : quantificateurs, copie et égalité
		6.1 Règles pour la logique du premier ordre
			6.1.1 Règles des quantificateurs
				6.1.1.1 Règles pour le quantificateur universel
				6.1.1.2 Règles pour le quantificateur existentiel
			6.1.2 Copie
			6.1.3 Les règles de l\'égalité
		6.2 Tactiques de preuves
			6.2.1 Raisonner en avant avec une hypothèse d\'existence
			6.2.2 Raisonner en arrière pour généraliser
			6.2.3 Un exemple d\'application des tactiques
		6.3 Cohérence du système
		6.4 Exercices
	Bibliographie