Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Séance de cours

Automatiser les preuves logiques de premier ordre en utilisant la résolution

Dans cours

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and ...

Description

Cette séance de cours présente la logique du premier ordre (FOL) et son application en mathématiques et en vérification de programme. Il couvre la syntaxe FOL, la sémantique, la satisfaisabilité, la validité, la skolémisation, la résolution et le processus de transformation des formules FOL en forme normale de négation et forme normale conjonctive.

Enseignant·e

Viktor Kuncak

Viktor Kunčak joined EPFL in 2007, after receiving a PhD degree from MIT. Since then has been leading the Laboratory for Automated Reasoning and Analysis and supervised at least 12 completed PhD theses. His works on languages, algorithms and systems for verification and automated reasoning. He served as an initiator and one of the coordinators of a European network (COST action) in the area of automated reasoning, verification, and synthesis. In 2012 he received a 5-year single-investigator European Research Council (ERC) grant of 1.5M EUR. His invited talks include those at Lambda Days, Scala Days, NFM, LOPSTR, SYNT, ICALP, CSL, RV, VMCAI, and SMT. A paper on test generation he co-authored received an ACM SIGSOFT distinguished paper award at ICSE. A PLDI paper he co-authored was published in the Communications of the ACM as a Research Highlight article. His Google Scholar profile reports an over-approximate H-index of 38. He was an associate editor of ACM Transactions on Programming Languages and Systems (TOPLAS) and served as a co-chair of conferences on Computer-Aided Verification (CAV), Formal Methods in Computer Aided Design (FMCAD), Workshop on Synthesis (SYNT), and Verification, Model Checking, and Abstract Interpretation (VMCAI). At EPFL he teaches courses on functional and parallel programming, compilers, and verification. He has co-taught the MOOC "Parallel Programming" that was visited by over 100'000 learners and completed by thousands of students from all over the world.

Source officielle

Proximité ontologique

Logique

Logique classique: Calcul des prédicats

Concepts associés (32)

Forme normale conjonctive

En logique booléenne et en calcul des propositions, une formule en forme normale conjonctive ou FNC (en anglais, Conjunctive Normal Form, Clausal Normal Form ou CNF) est une conjonction de clauses, où une clause est une disjonction de littéraux. Les formules en FNC sont utilisées dans le cadre de la démonstration automatique de théorèmes ou encore dans la résolution du problème SAT (en particulier dans l'algorithme DPLL). Une expression logique est en FNC si et seulement si elle est une conjonction d'une ou plusieurs disjonction(s) d'un ou plusieurs littéraux.

Règle de résolution

En logique mathématique, la règle de résolution ou principe de résolution de Robinson est une règle d'inférence logique qui généralise le modus ponens. Cette règle est principalement utilisée dans les systèmes de preuve automatiques, elle est à la base du langage de programmation logique Prolog. La règle du modus ponens s'écrit et se lit : de p et de "p implique q", je déduis q. On peut réécrire l'implication "p implique q" comme "p est faux ou q est vraie". Ainsi, la règle du modus ponens s'écrit .

Forme normale disjonctive

En logique booléenne ou en calcul des propositions, une forme normale disjonctive ou FND (en anglais, disjunctive normal form ou DNF) est une normalisation d'une expression logique qui est une disjonction de clauses conjonctives. Elle est utilisée dans la démonstration automatique de théorèmes. Une expression logique est en FND si et seulement si elle est une disjonction d'une ou plusieurs conjonctions d'un ou plusieurs littéraux. Tout comme dans une forme normale conjonctive (FNC), les seuls opérateurs dans une FND sont le et logique, le ou logique et la négation.

Calcul des prédicats

En logique mathématique, le calcul des prédicats du premier ordre, ou calcul des relations, logique quantificationnelle, ou tout simplement calcul des prédicats, est un système formel utilisé pour raisonner et décrire des énoncés en mathématiques, informatique, intelligence artificielle, philosophie et linguistique. Il a été proposé par Gottlob Frege une formalisation du langage des mathématiques entre la fin du et le début du .

Forme normale algébrique

En logique mathématique, la forme normale algébrique d'une fonction booléenne est une formule qui est un ou exclusif de conjonctions de variables propositionnelles ; par exemple 1 ⊕ a ⊕ b ⊕ ab ⊕ abc (1 correspond à la conjonction vide). Toute fonction booléenne admet une unique forme normale algébrique de taille minimale. Pour construire une formule normale algébrique, on part d'une forme normale disjonctive. On remplace ensuite la négation de a par (1 ⊕ a). On applique ensuite les règles de distributivité et d'absorption (a ⊕ a) = 0.

Afficher plus

Séances de cours associées (27)

Logique proposée : Règles d'inférence

Couvre l'interprétation de la logique de proposition et des règles d'inférence pour l'implication, la conjonction et la double négation.

Logique principale : quantificateurs, FNC, DNF

Couvre Predice Logic, en mettant l'accent sur les quantificateurs, le FNC et le DNF.

Automatiser les preuves logiques de premier ordre en utilisant la résolution

Couvre la syntaxe logique de premier ordre, la sémantique et la résolution pour les propriétés de preuve.

Automatiser les preuves logiques de premier ordre en utilisant la résolution

Couvre la logique de premier ordre, les preuves de résolution, les fonctions Skolem et la vérification de la satisfaction en mathématiques et la vérification de programme.

Proposition de résolution

Explore l'exhaustivité dans la logique propositionnelle, la résolution sur les clauses, la forme conjonctive, la résolution unitaire, les solveurs SAT et la génération de preuves.

Afficher plus

Concepts associés (32)

Forme normale conjonctive

Règle de résolution

Forme normale disjonctive

Calcul des prédicats

Forme normale algébrique

Afficher plus