Auteur
Patrick Dehornoy
Œuvres
Documents
Resume Une logique formelle consiste en un ensemble de formules generalement des mots avec une notion syntaxique de preuves generalement des suites de formules obeissant a des regles de deduction et une notion semantique de valeur determinee a l'aide de realisations convenables Les formules de la logique propositionnelle L sont des assemblages de variables X i a l'aide de connecteurs L'evaluation d'une formule de L se fait inductivement a partir de l'affectation de valeurs aux variables Une formule est dite valide resp satisfaisable si sa valeur est pour toute affectation resp pour au moins une affectation On dit que H se deduit par coupure a partir de F et G si G est la formule F H Une preuve par coupure est une suite de formules dont chacune est soit un axiome pris dans un liste fixee de types de formules soit obtenue par coupure a partir de formules anterieures de la liste Le theoreme de completude affirme qu'une formule de L est valide si et seulement si elle est prouvable Le theoreme de compacite affirme qu'un ensemble T de formules de L est satisfaisable c'est a dire qu'il existe une affectation de valeurs qui rende vraie chaque formule de T si et seulement si tout sous ensemble fini de T l'est De nombreux problemes peuvent etre codes en un probleme de satisfaisabilite ou de validite pour un ensemble de formules propositionnelles Le theoreme de Cook et Levin affirme le caractere NP complet de l'ensemble sat des formules satisfaisables
Documents
Etudes supérieures
Resume Une logique formelle consiste en un ensemble de formules generalement des mots avec une notion syntaxique de preuves generalement des suites de formules obeissant a des regles de deduction et une notion semantique de valeur determinee a l'aide de realisations convenables Les formules de la logique propositionnelle L sont des assemblages de variables X i a l'aide de connecteurs L'evaluation d'une formule de L se fait inductivement a partir de l'affectation de valeurs aux variables Une formule est dite valide resp satisfaisable si sa valeur est pour toute affectation resp pour au moins une affectation On dit que H se deduit par coupure a partir de F et G si G est la formule F H Une preuve par coupure est une suite de formules dont chacune est soit un axiome pris dans un liste fixee de types de formules soit obtenue par coupure a partir de formules anterieures de la liste Le theoreme de completude affirme qu'une formule de L est valide si et seulement si elle est prouvable Le theoreme de compacite affirme qu'un ensemble T de formules de L est satisfaisable c'est a dire qu'il existe une affectation de valeurs qui rende vraie chaque formule de T si et seulement si tout sous ensemble fini de T l'est De nombreux problemes peuvent etre codes en un probleme de satisfaisabilite ou de validite pour un ensemble de formules propositionnelles Le theoreme de Cook et Levin affirme le caractere NP complet de l'ensemble sat des formules satisfaisables
23 pages
Français