Introduction à la Logique

Résumé du document

En logique : un raisonnement valide utilise des règles d'inférence valides.
Une règle d'inférence permet le passage d'un certain nombre de prémisses à une conclusion.
Une règle d'inférence est valide à cause de sa forme et non pas à cause du sens des prémisses, par exemple, la règle Modus Ponens (...)

Extraits

[...] Rq: Une preuve n'utilisant que la règle Modus Ponens est une déduction sans hypothèses. II. Logique des propositions Théorie de la preuve : Méthodes axiomatiques (suite) Lemme 1 : La règle de Modus Ponens préserve la validité : Si = A et =  alors = B . Lemme 2 : La substitution uniforme préserve la validité : Soient A et B des formules et p une proposition atomique: Si = A alors = A[p\B]. II. Logique des propositions Théorie de la preuve : Méthodes axiomatiques (suite) Théorème 1 : Adéquation d'une preuve Si A est prouvable alors A est valide : Si - A alors = A. [...]

[...] Historique & Introduction Introduction En logique: un raisonnement valide utilise des règles d'inférence valides. Une règle d'inférence permet le passage d'un certain nombre de prémisses à une conclusion. Une règle d'inférence est valide à cause de sa forme et non pas à cause du sens des prémisses, par exemple, la règle Modus Ponens : A A  B B I. Historique & Introduction Introduction (fin) Parmi les règles d'inférence valides, citons : Règle Modus Tollens : ¬B A  B ¬ A Règle du Syllogisme : A  B B  C A  C Règle de Résolution : ¬X  A X  B A  B II. [...]

[...] Lorsque une telle preuve existe on peut la noter : S - res C II. Logique des propositions Théorie de la preuve : Méthode de Résolution (fin) Théorème 13: Validité d'une preuve par résolution Soit S un ensemble de clauses et C une clause , Si S - res C alors S = C. Remarque : La preuve par réfutation d'une clause C à partir d'un ensemble de clauses S est une déduction par résolution de la clause vide à partir de l'ensemble S  { qu'on appelle, plus brièvement, réfutation. [...]

[...] Logique des propositions Théorie de la preuve : Méthode de Résolution (suite) Algorithme de résolution par réfutation Soit C Cn} un ensemble fini de clauses : Soit G une clause à prouver: Remplacer S par S  {G} (S S  . Si on peut choisir une nouvelle paire de clauses C1 et C2 dans S telqu'il existe p atome avec p  C1 et  p  C2 alors calculer le résolvant R de C1 et C2. Si R la preuve est faite. Sinon, S S  et retourner à l'étape 2 Sinon (plus de choix possibles) alors S est consistant. II. [...]

[...] Sinon elle est dite ouverte. Définition 10 : clôture universelle d'une formule La clôture (ou fermeture) universelle d'une formule A(x xn) est la formule close A'=  x  xn A(x xn) . III. Logique des prédicats Langage des prédicats : LP1 (suite) Définition 11 : clôture existentielle d'une formule La clôture (ou fermeture) existentielle d'une formule A(x xn) est la formule close  x  xn A(x xn) . Définition 12 : formules propres Une formule A est dite propre lorsque : Il n'existe pas de variable dans A qui à la fois, des occurrences libres et des occurrences liées. [...]