Logique Mathématique

Description du programme de la matière:
A l’issue du cours, l’étudiant doit savoir faire la différence entre syntaxe et sémantique, savoir formaliser l’énoncé d’un problème et savoir utiliser la théorie des modèles ou la théorie de la démonstration pour montrer la satisfiabilité (non satisfiabilité) de cet énoncé. L’étudiant doit également maîtriser les propriétés de consistance et de complétude d’un système logique.

ID Cours
LOGM
Niveau
2ème année CP
Semestre
Semestre 4
Crédit
4
Volumes Horaires Cours
30.00
Coef
4
Volumes Horaires TD
30.00
Domaine
Sciences de l'ingénieur

Pré-requis:

Familles de Compétences

  • CF6 : Concevoir des systèmes orientés données et/ou d’aide à la décision

Type de compétence: 

TEC : Technique

MET : Méthodologique

MOD : Modélisation

OPE : Opérationnel

Niveau de compétence:

Base Intermédiaire Avancé
Famille de Compétence Compétence Elément de Compétence Type
CF6 C6.5: Formaliser l’énoncé d’un problème et analyser sa satisfiabilité C65.1: Exploiter une logique propositionnelle pour formaliser l’énoncé d’un problème MOD
C65.2: Utiliser la théorie des modèles ou de la démonstration pour montrer la satisfiabilité de l’énoncé d’un problème MOD

Contenu

I. Théorie des ensembles (rappels) (4h30h)
Fonctions
Relations
Ensemble et parties d’un ensemble,
Ensembles dénombrables
II. Le calcul propositionnel (15h30)
Introduction
Proposition et paradoxe
Syntaxe du langage propositionnel
L’alphabet
Les règles d’écriture
Etude Sémantique du langage propositionnel
Tableau de vérité d’une formule
Satisfiabilité
Conséquence logique
Système complet de connecteurs, les connecteurs de Sheffer
Propriétés des connecteurs logiques
Formes normales
Arbre sémantiq
YThéorie de la démonstration en calcul des propositions
Introduction
La résolution en calcul des propositions
Consistance et complétude de la résolution
Les stratégies de résolution

III. Le calcul des prédicats du premier ordre (40h

Introduction aux langages du premier ordre
L’alphabet
Les expressions du langage (termes et formules)
Système complet de connecteurs
Champ d’un quantifieur
Variables libres, variables liées, termes libres pour une variable
Etude Sémantique du langage des prédicats du premier ordre
Interprétation d’un terme
Interprétation d’une formule
Satisfiabilité d’une formule
Modèle d’une formule
Formule valide
Satisfiabilité d’un ensemble de formules
Modèle d’un ensemble de formules
Conséquence logique
Forme normale conjonctive et forme normale disjonctive
Forme normale prénexe
Forme de Skolem
Forme clausale
L’univers de Herbrand
Interprétation de Herbrand (H-interprétation)
Arbre sémantique
Théorie de la démonstration
Introduction à la théorie de la démonstration en calcul des prédicat
La résolution en calcul des prédicats
Substitution
Composition de substitutions
Unification
Principe de la résolution
Consistance et complétude de la résolution en calcul des prédicats
Les stratégies de résolution

Travail personnel

Bibliographie

Chang, Char-Tung Lee., “Symbolic Logic and Mechanical Theorem Proving”, Academic Press, Inc. 1973.
Kleene, “Logique mathématique”, Collection U, 1973.
Mendelson. D., “Introduction to Mathematical Logic”, Van Nostrand Company. 1979.

We are using cookies to give you the best experience. You can find out more about which cookies we are using or switch them off in privacy settings.
AcceptPrivacy Settings

GDPR