Logo ESI
Bannière
ESI talents

Bienvenue



Retour - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

Syllabus LOGM
Télécharger



Crédits : 4

LOGM
Logique Mathématique
Mathematical Logic

Coef : 4
VH Cours : 30.00
VH TD : 30.00
Pré-requis :

Ingénierie des Compétences

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

Description du programme de la matière

Objectifs:

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.

Contenu:

CONTENU DU MODULE :

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.

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -