A+Augmenter la taille du texteA-Réduire la taille du texteImprimer le documentEnvoyer cette page par mailPartagez cet articleFacebookTwitterLinked In
Number of hours
Lectures : 18.0
Tutorials : 18.0
Laboratory works : -
Projects : -
Internship : -
Written tests : -
ECTS : 3.0
Officials :Nils GESBERT
Classical and non-classical logics pervade all aspects of Computer Science. They are essential, among other things, in assuring software quality. Computer scientist therefore need to be familiar with concepts and techniques related to formal systems and automated inference. This course is particularly relevant to ISI and SLE students.
1. Propositional logic : semantic tableaux, Davis and Putnam’s method, resolution, formal systems, compactness theorem. Algebraic approach to propositional logic.
2. First-order terms. Term equations. Substitutions. Unification algorithm.
3. First-order logic. Expressiveness. Semi-decision procedure. Prenex normal form, Lowenheim-Skolem theorem, Herbrand theorem. Semantic tableaux and resolution methods.
4. Programming with logic, specification, strategy. Illustrative programs.
1 written examination (3h) at the end of the period.
N1 = (E1 + E2)/2 N2 = E3
The course exists in the following branches:
Curriculum - Work Study Education - Alternance 1ere annee