Remerciez-le!

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

Poly copie log i que 1 Éléments de Logique pour le cours de ème année Ensimag Fondements de Logique pour l ? Informatique Thierry Boy de la Tour Mnacho Echenim Année - C CTable des matières Inférences et logiques Introduction Systèmes d ? inférence Logiqu

Éléments de Logique pour le cours de ème année Ensimag Fondements de Logique pour l ? Informatique Thierry Boy de la Tour Mnacho Echenim Année - C CTable des matières Inférences et logiques Introduction Systèmes d ? inférence Logiques Exercices supplémentaires Logique propositionnelle Dé ?nitions Un système d ? inférence Forme clausale Renommage Résolution DPLL Compacité La logique du premier ordre Termes atomes et formules du premier ordre Interprétations valuations substitutions La relation de satisfaction Le théorème de Herbrand Formes normales et skolemisation Conséquences générales du théorème de Herbrand Uni ?cation Forme clausale Résolution et factorisation Exercices corrigés C TABLE DES MATIÈRES Ce polycopié est constitué des dé ?nitions et preuves des résultats qui seront étudié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 énoncé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 notions 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? wenheimSkolem 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 CTABLE DES MATIÈRES 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