Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

Éléments de Logique pour le cours de 2ème année Ensimag: Fondements de Logique

Éléments de Logique pour le cours de 2ème année Ensimag: Fondements de Logique pour l’Informatique Thierry Boy de la Tour Mnacho Echenim Année 2017-2018 Table des matières 1 Inférences et logiques 9 1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.2 Systèmes d’inférence . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.3 Logiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 1.4 Exercices supplémentaires . . . . . . . . . . . . . . . . . . . . . . . . 19 2 Logique propositionnelle 23 2.1 Déﬁnitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 2.2 Un système d’inférence . . . . . . . . . . . . . . . . . . . . . . . . . . 29 2.3 Forme clausale . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 2.4 Renommage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 2.5 Résolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 2.6 DPLL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 2.7 Compacité . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 3 La logique du premier ordre 47 3.1 Termes, atomes et formules du premier ordre . . . . . . . . . . . . . . 49 3.2 Interprétations, valuations, substitutions . . . . . . . . . . . . . . . . 53 3.3 La relation de satisfaction . . . . . . . . . . . . . . . . . . . . . . . . 56 3.4 Le théorème de Herbrand . . . . . . . . . . . . . . . . . . . . . . . . 62 3.5 Formes normales et skolemisation . . . . . . . . . . . . . . . . . . . . 66 3.6 Conséquences générales du théorème de Herbrand . . . . . . . . . . . 74 3.7 Uniﬁcation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 3.8 Forme clausale . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 3.9 Résolution et factorisation . . . . . . . . . . . . . . . . . . . . . . . . 86 4 Exercices corrigés 93 3 4 TABLE DES MATIÈRES Ce polycopié est constitué des déﬁnitions et preuves des résultats qui seront étu- diés dans le cours de Logique au premier semestre de la deuxième année à l’Ensimag. C’est un support de cours qui doit servir de référence aux étudiants et qui n’est pas destiné à remplacer la présence en classe. Il est divisé en trois chapitres : Inférences et logiques. Ce chapitre permet de comprendre comment des énon- cés peuvent être engendrés à partir d’autres énoncés (systèmes d’inférence), comment attribuer une valeur de vérité à ces énoncés (logiques), et les liens entre ces deux notions. Ce chapitre assez abstrait sert de base pour tout ce qui suit dans le cours de logique. La logique propositionnelle. Ce chapitre déﬁnit dans un cadre général les no- tions connues de variables booléennes, de tables de vérité... Puis diﬀérents systèmes d’inférence permettant de tester eﬃcacement la satisfaisabilité d’une formule sont présentés, ainsi que le théorème fondamental de compacité de la logique propositionnelle. La logique du premier ordre Ce chapitre déﬁnit de façon formelle la logique du premier ordre, puis présente les théorèmes de Herbrand et de Löwenheim- Skolem avant d’introduire l’opération d’uniﬁcation qui est très utilisée dans de nombreux domaines (Bases de Données, IA...), et la règle de résolution pour la logique du premier ordre. Ceci est la deuxième version du polycopié, il est certain qu’il contient encore des coquilles. Nous sommes reconnaissants à Cyril Lorenzetto pour sa relecture de la première version et la détection de nombreuses coquilles ; nous serons reconnaissants à tout lecteur qui nous signalera les coquilles restantes. TABLE DES MATIÈRES 5 Prolégomènes sur les ensembles Ce cours de logique s’appuye sur certaines notions issues des mathématiques modernes qui ne sont plus systématiquement enseignées et font parfois défaut aux étudiants. S’il n’est pas question de faire de tout ingénieur un mathématicien, il faut bien constater que l’informatique fait un usage intensif de notions comme les entiers, les nombres réels, les tableaux (qui ressemblent étrangement à des fonctions), les listes, les mots, les pointeurs (qui permettent de former des graphes), etc. Ce n’est pas un hasard si ces objets sont tous de nature mathématique. Écrire un algorithme c’est décrire une inﬁnité de calculs possibles et les mathématiques sont le seul outil intellectuel permettant d’assoir les raisonnements indispensables à une tâche aussi complexe. Une des causes de cette complexité est la nécessité de penser l’inﬁni. Or cette notion est historiquement l’une des plus controversée depuis l’antiquité et celle qui a fait dire le plus d’âneries teintées de mysticisme à des penseurs pourtant brillants, au point que Galilée considérait qu’il fallait l’éviter dans les raisonnements car elle menait inévitablement à des contradictions. Il est donc illusoire d’espérer faire mieux que ces antiques génies sans se donner des moyens dont ils ne disposaient pas. Car ces moyens existent, ils ont été découverts au XIXème siècle par Georg Can- tor et ils ont permis dans une large mesure de résoudre le problème de l’inﬁni. Et l’outil qui permet de penser l’inﬁni est précisément celui qui est au centre des ma- thématiques modernes, c’est la théorie des ensembles. S’il n’est pas question ici de développer cette théorie puisqu’on ne saurait le faire en quelques pages, il nous a ce- pendant semblé utile pour la compréhension du cours d’en décrire certains aspects. La notion d’ensemble fait partie de celles qui sont considérées comme suﬃsam- ment simples pour ne pas être déﬁnies bien qu’on y ait constamment recours. Tout le monde connaît l’ensemble vide ∅, l’ensemble N des entiers naturels et sait qu’une ﬁ- gure géométrique est (ou peut être vue comme) un ensemble de points. Les ensembles sont ainsi perçus comme des boîtes contenant divers objets mathématiques et notre expérience du monde physique est censée nous fournir une intuition suﬃsante de ce que sont les propriétés de ces boîtes. Pourtant, s’il est évident que l’ensemble A des multiples de 2 et l’ensemble B des multiples de 3 sont distincts, ces boîtes contiennent toutes deux l’entier 6 (qui ne s’est pas dédoublé lorsqu’on a déﬁni A et B). C’est même la boîte des multiples de 6 qui est entièrement contenue dans les boîtes A et B. On voit ainsi que les frontières de ces boîtes s’interpénètrent, ce qui nous éloigne radicalement du monde physique et laisse notre intuition un peu en déshérence 1. Sommes-nous alors libres d’imaginer et de déﬁnir ces frontières comme bon nous semble ? C’est ce qu’on a pu croire au XIXème siècle, mais la découverte du paradoxe de Russell au début du XXème siècle a montré que c’était une impasse. Il consiste 1. on utilise aussi les diagrammes de Venn comme support géométrique à l’intuition, mais ils deviennent vite illisibles ; on dépasse rarement le diagramme à quatre ensembles. 6 TABLE DES MATIÈRES à considérer l’ensemble E de tous les ensembles et parmi ceux-ci l’ensemble A des ensembles X qui ne se contiennent pas (X ̸∈X). Par exemple on a E ∈E donc E ̸∈A. Mais uploads/Philosophie/ poly-copie-log-i-que 1 .pdf