• Votre sélection est vide.

    Enregistrez les diplômes, parcours ou enseignements de votre choix.

Logique (INFO501_INFO)

  • Composante

    UFR Sciences et Montagne

Description

Introduction à la logique du premier ordre et ses applications en informatique (modélisation, satisfaction de contraintes, satisfiabilité, preuve de programmes)

Les TP permettront d’explorer différentes applications mentionnées en cours : implémentation partielle (en Python) et utilisation d’un SAT solveur, utilisation d’un assistant de preuves (Coq), introduction à Prolog.

Lire plus

Heures d'enseignement

  • CMCours Magistral6h
  • TDTravaux Dirigés9h
  • TPTravaux Pratiques12h

Pré-requis obligatoires

Mathématiques de L1

Lire plus

Plan du cours

1 – logique propositionnelle : syntaxe des formules, sémantique (tables de vérités et algèbres de Boole), modélisation de contraintes et problème de satisfiabilité, SAT solveur et algorithme DPLL, démonstrations (déduction naturelle), correction et complétude

2 – logique du premier ordre : syntaxe des termes, formules et quantificateurs, substitutions et renomage, résolution, algorithme d’unification de Martelli et Montanari, Prolog, sémantique, notion de modèle, démonstrations (déduction naturelle), théorème de complétude, exemple : arithmétique, théorème d’incomplétude

Lire plus