[PDF] [PDF] Cours Logique et Calculabilité - CNU 27 Marseille

View - Download [PDF] Cours Logique et Calculabilité - CNU 27 Marseille

Previous PDF

Next PDF

CoursLogique etCalculabilité

L3Infor matique2013/2014

TexteparSéve rineFrata ni,avecaddendaparLuigiS antocanale

Versiondu11février 2014

2

Tabledesmati ères

1Int roduction5

1.1Pou rquoilalogique?...... ... ...... ... .. ... ... ... ... ... 5

1.1.1Laf ormalisationdu langage... ...... ...... ... .. ... ... .5

1.1.2Laf ormalisationdu raisonnement. ...... ........... ... ... 5

1.2Logique etinforma tique. .................... ... ... ... ... 6

1.3Conten uducours.......... ..... ............... ... ... .6

2Ca lculpropositionn el7

2.1Introd uction.......................... ... ... ... ... .. 7

2.2Syn taxeducalculproposition nel:lesform ules.... .............. ..7

2.3Séman tiqueducalculpropositionnel ...... ...... .............. 8

2.3.1M odèlesd'uneformule. ............ ........... ... ... 10

2.3.2Lacon séquen celogique(d'unensembledef ormules).. ........ ...12

2.3.3Décidab ilitéducalculproposition nel.... ...... ............17

2.4Equ ivalenceentreformules.... ...... .............. ... ... ..18

2.4.1Lasu bstitution ........... ... ... ... ... .. ... ... ... 18

2.4.2Equ ivalencesclassiques.......... ..... ... ... ... ... ..18

2.4.3Formes normales.... ...... .. ... ... ... ... ... ... ... 19

2.5Lep roblèmeS AT....... ........ ... ... ... ... ... ... ... .21

2.5.1Défin itionduproblème... ...... ........ ... ... ... ... .21

2.5.2Unp roblème NP-complet........ ......... ... .. ... ... 21

2.5.3Mo délisation-RéductionàSAT. ... ......... ... ........ 23

2.5.4Algorithmes derésolutiond eSAT.. ...... ...... ........ .25

2.5.5Sou s-classesdeSAT.. ...... ......... ... ... .. ... ... 30

2.5.6LesSAT-solv ers...... ............................ 32

2.5.7App lications......... ... ... ... ... ... .. ... ... ... 33

2.5.8Su rlamodélisation... ... ........... ... ... ... ... ... 35

2.6Systèmes depreuv es..... ............ ... ... .. ... ... ... .36

2.6.1Lan otionde systèmeformel... ...... .. ...... ... ... ... .36

2.6.2Lamé thod edelacoupure...... ...... ... ............ .36

2.6.3Systèmes depreuv eàlaHilbert. ............ ... ... ..... .40

2.7Lesrègles ducalcu ld esséquents.. ...... ...... ........ ... ... 44

2.8Résumé ...... ... ... ... .. ... ... ... ... ... ... ... .. ..45

3Ca lculdesprédicats49

3.1Introdu ction........................... ... .. ... ... ..49

3.2Prélimin aires........ ... .. ... ... ... ... ... ... ... ... .. 49

3.2.1Lesf onctions ............ .. ... ... ... ... ... ... ... 49

3.2.2Lesrelation s.. ..... ... ... ... ... ... ... .. ... ... ..50

3.3Unexemp le.. ...... ... ... .. ... ... ... ... ... ... ... .. .50

3.3.1Interprétat ion1................................. .50

3.3.2Interpréta tion2................................. .51

3.3.3Interprétat ion3................................. .51

3.3.4Interpréta tion4................................. .51

3

4TABLEDESMATIÈRES

3.3.5Interpréta tion5................................. .51

3.3.6Interprétat ion6................................. .52

3.3.7Comparaiso ndesinterprétations.......... ......... .....52

3.4Exp ressionsetformules.... ... ............ ... .. ... ... ... 52

3.4.1Lestermes ... ... ... ... .. ... ... ... ... ... ... ... .52

3.4.2Lelan gage.. ..... ... ... ... ... ... ... .. ... ... ... 53

3.4.3Lesform ulesd ucalculdesprédicats. ..... ...... ...... ....54

3.4.4Occurren ceslibresetliéesd'une variable.. ... ... ............ 55

3.5Séman tique.......... ... .. ... ... ... ... ... ... ... ... .56

3.5.1Stru cturesetvaluations.... ..... ............ ... ... ..56

3.5.2Ev aluation........... ... ... ... ... ... .. ... ... ..57

3.5.3Unexemp le.. ...... ... .. ... ... ... ... ... ... ... ..58

3.5.4Vo cabulaire........... ... ... ... ... ... .. ... ... ..59

3.6Man ipulationdeformules...... ..... ............ ... ... ... 61

3.6.1S ubstitutiondevariables...... ...... ........ ... ... ... 61

3.6.2Equ ivalencesclassiques............. ...... ... ... ... .61

3.6.3Formes Normales.... ... ... ... ... ... ... ... .. ... ... 62

3.7Unifi cation....... ... ... ... ... ... ... ... .. ... ... ... .64

3.7.1Su bstitionsetMGUs...............................64

3.7.2Algorithme d'unification. .............. ... ... ... ... ..65

3.7.3Correctione tcompletude............... ..... ........66

3.8Résolution ..... ... ... ... ... ... ... .. ... ... ... ... ... .68

3.8.1Su bstitution,surlesformulespropostionn elles..... ... .........68

3.8.2Lesr ègl esducalculdelarésolution.... ...... ...... ..... .69

3.8.3Utilisationd 'un démonstrateurautomatique.. ............ ....72

4Ca lculabilité77

4.1Mac hinesdeTuring...... ..... ............ ... ... ... ... 77

4.2Prob lèmesdedécision.... ...... ..... ... ... ... ... ... ... .78

4.3Unp roblèmein décidable.... ............... ... .. ... ... ... 79

4.4Thèsede Chruch...... ...... ............... .. ... ... ..79

4.5Indeci dabilitédelalogiquedupremierordre..... ...... ..... ......79

Chapitre1

Introduction

1.1Pourquoi lalogique?

1.1.1La formalisationdu langage

Lemotlogiqueprovientdugreclogos(raison,discours),etsig nifie"sciencedelaraison".Cette scienceapourobjetsd'é tu delediscours etleraisonnement. Ceux-cidépendentbiene ntendu du langageutilisé .Sionprendlelangagec ourant,ons eren dcomptefacilement: - qu'ilcontien tdenombreusesambigu ïtés:nou snesommespastoujourssûrsdelasémantique d'unénoncéo ud'unephrase.Par exemple:"no usavons desjumellesàlamai son».(Deux fillesoudeslunet tesoptiq ues?)O u"ilatrouvéuna vocat»(leprofessionneloule fruit?) - qu'ilestd i!ciledec onnaîtrelavé racitéd'unénoncé:" ilple uvrademain»,"Jeane st laid», "lalogiquec 'est dur ». - qu'ilperme td'énoncerdesc hosesparadoxales: c'estvraia lorsc'estfaux... etinversement.

3.Unarrê téenjointaub arbier(masculin)d'unvillagederas ertou sleshommesduvillage

quinese rasentpas eux-mêmes etseulementce ux-ci.Leb arbiern'apaspurespecter cetterèglecar: - s'ilseraselui -même,i lenfreintl arègle,carlebarbiernep eutraserque leshommes quinese rasentpas eux-mêmes ; - s'ilneserasepasl ui-mêm e(q u'ilsefasser aserouq u'ilconservelabarbe), ilesten tortégale ment,carilalachargederaserle shommesqu ine seras ent paseux-mêmes.

4.ParadoxedeRussel:c'es tlaver sionmathématiqued upa radoxedubarbier :soit a

l'ensembledesensemblesquinese contienn entpaseux-même.Cetensemblen 'existepa s caronp eutv érifierquea!assia/!a. Toutcecifait queleslangu esnaturelles nesontpas adaptées auraisonnementformel .C'est pourquoiparexemple,on vousaappr isunlangagespécifiquepourf airede spreuvesenm ath éma- tique.Unepreuv emathématique nepeutêtrefaiteenutilisan ttoutlevocabulaired elalangue

naturellecarlesénoncésetlespr euvesdeviendra ientalo rsambiguës.L ela ngageuti liséenmathé-

matiqueestcelui delalogique classique(enr éalité,c'estun langageunp euplus souple,entr ela logiqueclass iqueetlalanguenaturelle).

1.1.2La formalisationdu raisonnement

Unefoisle langageformalisé, cequ iintéress eleslogiciensc'est leraisonneme nt,eten particulier,

ladé finitiondesystèmesformelsp ermettantde mécaniserleraisonnement. Audébutdu20iè me siècle,lerêve dulogicien estdefairedelal ogique uncalculetdemécaniserleraisonnement et résultatd'incomplétu de:ilexistedesénoncésd'arithmétiquequine sont pasp rouvableparun 5

6Chapitre1.Introduction

systèmeformeldepreuv e.Iln'existedoncpa sd'alg orithmequipermettede sav oirsiunénoncé mathématiqueestvr ai.

1.2Logiq ueetinformatique

Malgrécerésultatnégati f,l' arrivéedel'informat iqueàpartirdesannées30ma rquel'essorde

lalogique . Elleestprésenteda nsq uasimenttouslesdomaines del'infor matique: - vousverrezp arexempleencou rsd'archi tecturequevotreordina teures tformédecircui ts logiques. - laprogrammation n'estau fondquedelalogique.Dan sles année60,lacorres pondanc e deCurry -Howard,établieunecorrespondancepre uve/programme:unerel ationent reles démonstrationsformellesd'unsystèmelogique etlesprogrammesd'unmodèle decalcul. - letraiteme ntautomatiquedeslangue s, - l'intelligenceartificielle, - lalogique apparaitégale mentdanstoutes lesquestionsdesureté. Onde mandemaintenantdeplusenp lusdeprouverlasuretédes programmes etdespro- tocoles.Pourcelaonmod éliselesexéc utionsdesprogramme s,on exprimelespropriétésde sûretéparuneformule logiq ue,puis onvérifiequelesmodèl essatisfontbienlaformul e.

Acettee

quipermet tentderaisonnersurl'évolution decert ainssystèmesaucoursdutemps .Ilexiste mêmedeslogiques pourfor maliserles règlesdespare-feu,a find'éviter d'avoir dessystèmes derèg leincohérents. - etplei nd'autresquej' oublie. Ilex isteégalementdesl ogicielsquipermettentdepro uverdesfo rmuleslogique(automatique- mentousemi-automatiquement). Enparticulier onadeslogicielsper mettantde générerducode

vérifié:onentreun eab strac tionduprogramme aréaliser ,onprouvesurcetteabstractiondefa çon

plusoumoi nsautomat iquemaissûre,l espropriétésdesûretésouhaitées;etlelog icielproduitdu

codecertifié. L'informatiqueestdoncin dissociablede lalogique.Heureus ementtoutboninformaticienn'est

pasoblig éd'êtreunbonthéoricien delalogique,ma isi ldoitêtrecapa blemaitrisersonutilisati on.

1.3Contenu ducours

Ons'in téresseraprincipalementà(desfragme ntsde)lalogiqueclassique,quiestlalogique utiliséepourlesmathémati ques,etformelaba sedepresque touteslesautreslogiques. Nousallonsn ousintéres serauxfragment suivants: - lalogique propositionn elle; - lalogique dupremie rordre. Pourchacun edeceslogiques,nousn ouspos eronsprin cipalementlesquestionssuiva ntes: - Quelleestsasyntaxe ?I.e.,com mentéc rireunephrasedanslelang agedelalogiq ueconsidéré. - Quelestsasé mantique? C'est-à -dire,étantunephrase,savoirluia ttribuerunsens.Cette questionouvreàuneau trequiest "dequ elformesontles modèles d'uneform ule",c'est univers? - Lalogique estel le-décidable? Etantdonnéunephrase(formule)dulangage,existe-ilune procéduree ectivepermettant d'évaluercetteformule. - Existe-ilunsystèmeformel decal culpermettantde"prouver "qu'unénoncéestv rai ou faux. D'autresquestionss eposentévidementmaiss esontprin cipalementcelles-ciqui intéressentl'in- formaticien.

Chapitre2

Calculpropositionne l

2.1Introduc tion

Lesformu les(ouphrases,ouénoncé s)d ucalculpropositionnelsontde deu xtypes:oubien unefor muleestunepropositionatomique,oubienelleestcomposéeàpartird'autresformules propositionnels). Considérons,parexemple,l'énoncéar ithmétiq ue"2+2=4ou3+3=5».Ce tén onc épeuts e considérercommeconstruit desprop ositionsatomiques"2+2= 4»et "3+3=5»,vialeconnecteur

considèrel'énoncé"s' ilpleut,alors lesol eilsecache»,quel 'onreconnaîtraêtreéq uivalentà"il

pleutimpl iquequelesoleilsecache»,comme obtenudesdeux proposit ionsatomiques"s' ilpl eut» et"l esolei lsecache»v ialeconnecteurproposi ti onnelimplique. Uneproposition atomiqueestuné noncésimple,nepouvant prendrequele svaleurs "vrai"ou "faux",etcedef açonnon ambigu ë;elle donned oncunein formationsurun étatdechose.De plusuneprop osit ionatomiqueestindécomposable:"lecielestbleu etl'herbeestverte»n'est pasuneprop osit ionatomiquemaislacompositiondedeuxpro positionsatomiques.Dansl 'analyse dula ngagenaturel,onnepeutpasconsi dérercommedespropositions :lessouha its, lesphrases impérativesoulesinterrogations. Nousavonsdé jàvudesexemples deformulesc omposé es.Considé ronsmaintenantl'énoncé "s' ilneige,alo rslesoleilsecache etilfaitfroid». C'estun eformulecomposée, vialec onnecteur froid».Onpeutdoncco mpose rdesformul esàpart ird'autr esformulescomposées.Lavaleur de véritéd'uneformul ecomposéesecal culecommeunefoncti ondesformulesdontellees tcomp osée. Lecalc uldespropositionses tlapremièreétap edansladéfinitiondelalogique etdurai- sonnement.Ildéfinitles règlesdedéduct ionquir elientles phrasesentreelles, sansenex aminer lecon tenu;ilestainsiunepremiè reétap edanslacons tructionducalcul desprédicats, quilui s'intéresseaucontenudespropositi ons. Nouspartirons doncengénéral defaits:"pest vrai,qestf aux"etessaieronsd edétermine rsi unea rmationparticulièreestvr aie.

2.2Syntax educalculpropositionnel: lesfo rmules

Lelangageducal culpropositi onnelestforméde:

- symbolespropositionnelsProp={p 1 ,p 2 - connecteurslogiques{¬,",#,$}; - symbolesauxiliaires:par enthèsesetespace. Remarque2.1.Danslalittérature logiqueon utiliseplusieurs synonymes pour symboleproposi- tionnel;ainsivariablepropositionnelle ,propositionatomique,formuleatomique,ouencoreatome sonttou sdessynonymesdesymbolepropositionnel. 7

8Chapitre2.Calculproposi tionn el

L'ensembleF

cp desformulesducal culproposition nelestlepluspetitensembletelque: - toutsymb olepropositionnelestu neformule; - si!estunefor mule alors¬!estunefor mul e; - si!,"sontdesformul esalor s!#",!""et!$"sontdesform ules. Lessymb olesauxiliairesnesontutilisésqu epourleverle sambiguï téspossibles: parexemple, laform ulep#q"restambi guë,carellepeutse lir ededeuxfaçonsdi"érentes,((p#q)"r)oubien (p#(q"r)). Exemple2.2.p,p$(q#r)etp#qsontdesformul esprop ositionnelles;¬(#q)etf(x)$g(x) n'ensont pas. dontlesfeuilles sontét iquetéspardessymbol espropositionnelset lesnoeudspardesconnecteurs. Parexe mple,laformulep$(¬q"r)correspondàl'arbrer eprésent éFigure2.2. q p" ¬r Figure2.1-R eprésen tationarborescentedelaformulep$(¬q"r) Notation2.3.Onutilis esouvente nplusleconnecteurbinaire%commeabr éviation:!%"est l'abréviationde(!$")"("$!).Delamêmefaçon,onajoutelesymbole&quicorresp ondà Fauxetle symbole'quicorresp ondàVrai.Cesdeuxsymbolessontaussidesabréviations,ilsne sontpasindi spensables aulangage.(Parexemple&peutêtreut iliséàlaplac edep"¬pet'àla placedep#¬p.) Définition2.4(Sous-formule).L'ensembleSF(!)dessous-fo rmulesd'uneformules!estdéfini parinductio ndelafaçonsuivante. - SF(p)={p}; - SF(¬!)={¬!}(SF(!); - SF(!)")={!)"}(SF(!)(SF(")(où)désigneundessymbo les ",#,$). Parexem ple,SF(p$(¬q"r))= {p,q,r,¬q,¬q"r,p$(¬q"r)}.Quandonvoituneformule commeunar bre, unesous-formuleestsimplemen tunsous-ar bre(voirFigure2. 2). Définition2.5(Sous-formulestricte)."estunesous -form ulestrictede!si"estunesous -for mule de!quin'est pas!.

2.3Sémantiq ueducalculpropositionnel

Ilfa utmaintenant unmoyendedéterminersiuneformu leest vraieoufausse.L aprem ière

étapeestdedonneruneval eurdev érit éauxpr oposi tionsatomiques.L' évaluat iond'uneformule,

dépenddoncdesvale urschoisiesp ourlessy mbolespropositionnel s.Cesvaleurssontdonnéesp ar unevaluation. Définition2.6(Valuation).Unevaluatione stuneapplic ationdePropdans{0,1}.Lavaleur0 désignele"faux "etlava leur1désignele"vra i".

2.3Séman tiqueducalculpropositionnel9

q p" ¬r Figure2.2-Re pr ésentationarborescentedessous-formulesdep$(¬q"r) Unevaluations erasouvent donnéesousf ormed'untableau.Parexemple,s iProp={p,q} alorslav aluationv:p*+1,q*+0s'écritplussimplementv: pq 10 Unefoislav aluationvchoisie,lavaleurdelaf ormules edéterminedefaçon nature lle,pa r extensiondelavaluati onvauxformules delafaçonsuivante:

Définition2.7(Valeurd'uneformule ).

- v(¬!)=1ssiv(!)=0; - v(!#")=1ssiv(!)=1ouv(")=1; - v(!"")=1ssiv(!)=1etv(")=1; - v(!$")=0ssiv(!)=1etv(")=0. Ladé finitionprécédentepeu tapparaîtretrompeusecarcircualire:afind'explique rlalogique, noussommeen trainde l'ut iliser(ssi,ou,et...).Parai lleurs,on peutseservirdeladéfinition suivantequiestene etéqui valenteàlaDéfinition2.7:

Définition2.8(Valeurd'uneformu le(bis)).

- v(¬!)=1,v(!); - v(!#")=m ax(v(!),v(")); - v(!"")=min(v(!),v(")); - v(!$")=v(¬!#"). Cettedernièr edéfinitionestpurementco mbinatoirecarellereposesur lastructu redel'ensemble qu'iln'ya pasbesoin dela justifier pard'autresmoyens . Exercice2.9.Proposezunalgorithme qui, étantdonnéuneformule!ducal culpropositi onnelet uneva luationv,calculev(!).Queltypedestructurededonnéesutiliserpourcoderlesformules? Queltyped estructurededonné esutiliser pourcoderlesvaluations ? Notezquelad éfinition 2.8corre spondauxtablesdevéritédesc onn ecteurslogiques(dontvous avezsûre mententenduparler): p¬p 01 10 pqp"q 000 010 100
111
pqp#q 000 011 101
111
pqp$q 001 011 100
111
Remarque2.10(Langagenature letlangageformel).Remarquezladéfi nitionp articulièrede

l'implication:onl'ente nde ngén éralcommeun"si...,alors...",onvoitic iquel'én oncé"si1+1=1,

alorslacap italed elaFranceest Marseille"estvrai,pu isquetou tephrase!$"estvr aiedès

10Chapitre2.Calculpropos itionn el

lorsque !estévalu éeàfaux.Ceciestpeunatu re l,cardanslelang agecoura nt,onnes' intéresse à

lavé ritéd'untelén oncéquelorsqu elacondition estvraie:"s'ilfaitbeaujev aisàlapêc he"n'a

d'intérêtpratiqueques'il faitbeau...Attribuerlav aleurvr aidanslecaso ulaprémisseestfa usse correspondapeuprèsàl 'usa gedusi..al orsdanslaphr asesuiv ante:"SiPierreobtientsa Licence, alorsje suisEinstein" :c'estàdirequ epartantd'unehypoth èsefau sse,alors jep euxdémontrer descho sesfausses(ouvr aies).Parcon tre,iln'estpa spossiblededémontrerquelquecho sedefaux partantd'unehypothèsevr aie.

D'autresexemples oùilestdi

ciledec oderlelan gagenaturelvialelangageformel: - commentcoder iezvous,enlangageformel,l' énoncéfrançais"Soi tilestfr ais,soitil est chaud»? - etcomment coderiez vousl'énoncéanglais"EitherIcannotunderstand French,or my professordoesn'tknowhow tospeakit» ? Onpe utajouterladéfi nitiondelavaleurdel'abréviation%:v(!%")=1ssiv(!)=v("). Cequ icorresp ondàlatabledevéritésuivante: pqp%q 001 010 100
111
!!F cp ,parinductioncommesuit:

Prop(p)={p},

Prop(¬!)=Prop(!),

Prop(!)")=Prop(!)(Prop("),)!{",#,$}.

Montrezque:

- Prop(!)=Prop-SF(!),pourtout!!F cp - siv(p)=v (p)pourtoutp!Prop(!),alorsv(!)=v

2.3.1M odèlesd'uneformule

Définition2.12.L'ensembledesvaluationsd'unensemblede variablespr opo sitionnellesProp estnoté Val(Prop)(ouju steVallorsqu'iln'yapas d'ambiguités urProp).Val(Prop)estdonc l'ensembledesfonctionsdePropdans{0,1}. Parexe mple,siProp={p,q,r},alorsValestrepr ésentéparlaTable2.3.1,dansl equelc haque ligneestu nevaluationdeProp: pqr 000 001 010 011 100
101
110
111
Table2.1-L'e nsem bleVal(Prop)desva luationsdeProp={p,q,r} Définition2.13(Modèled'uneformule) .Unmodèlede!estunev aluat ionvtelleque v(!)=1.

Onnote mod(!)l'ensembledesmodèlesde!.

2.3Séman tiqueducalculpropositionnel11

Exemple2.14.SiProp={p,q,r}et!=(p#q)"(p#¬r)alorsl'ensem bledesmodèlesde!est mod(!)= pqr 010 100
111
110
111
Définition2.15(Satisfaisabilité).Uneformu le!estsatisfaisable(ouconsistante,ouencore mod(!).=!). Définition2.16(Insatisfaisabilité).Uneformule !estinsatisfaisable(ouinconsistante,ou mod(!)=!) Définition2.17(Tautologie).Uneformu le!estunetautologie(ouvalide)siv(!)=1pour toutevaluationv(i.e.,simod(!)=Val).Onn ote|=!pourdireq ue!estunet autologi e. Unexe mpledetautologieest!#¬!,c'estàdireletiersexclus. Exercice2.18.Montrezquelesformules suivantes sontdesta utologies: Définition2.19(Equivalence).Ondit que!estéquiv alenteà"siles deuxformules ontl es mêmesmodèles (i.e.simod(!)=mod(")).Onn otealors!/". Exemple2.20.Lesopérateu rs",#sontassociat ifs-commutatifs.Deuxformulesidentiquesà associativité-commutativitéprèssontéquivalen tes.Remplacerune sous-formule"d'uneform ule !parunefor mule équivalente" donneunefor mule notée!["0" ].Cet tesubstituti onpréserve lesmodèle s,i.e.,mod(!)=mod(!["0"

Exercice2.21.Prouvezleséquiva lencessuivantes:

Proposition2.22.Soient!et"deuxformul es,ona:

1.mod(¬!)=Val,mod(!);

2.mod(!#")=mod(")(mod(");

3.mod(!"")=mod(")-mod(");

4.|=!$"ssimod(!)1mod(").

Démonstration.1.pourtoutev aluationv!Val,

v!mod(¬!)ssiv(¬!)=1 ssiv(!)=0 ssiv/!mod(!) ssiVal,mod(!)

2.pourtoute valuationv!Val,

v!mod(!#")ssiv(!)=1ouv(")=1 ssiv!mod(!)ouv!mod(") ssimod(!)(mod(")

12Chapitre2.Calculpropos itionn el

3.pourtoutev aluationv!Val,

v!mod(!"")ssiv(!)=1etv(")=1 ssiv!mod(!)etv!mod(") ssimod(!)-mod(") 4. |=!$"ssipour touteval uationv!Val,v(!$")=1 ssipour toutevaluat ionv!Val,v(¬!#")=1 ssipour toutevaluat ionv!Val,v(!)=0ouv(")=1 ssipour touteval uationv!Val,v(!)2v(") ssimod(!)1mod(") Définition2.23(Conséquencelogique).Uneformule "estconséquencelogiqued'uneformul e !sitout modèlede!estunmo dèle de"(i.e.,simod(!)1mod(")).Onn otealors!|=". Remarque2.24.Attentionàlaconfusiondan sle sdeuxn otations! - v|=!oùvestunev aluati on,i.e.,l'assignationd'unev aleurauxpropositionsatomi ques dela formule; c'estunraccourcisassezfréquentpo urv(!)=1; - "|=!où"estunefor mul e. Proposition2.25.Soient!et"deuxformul espropositionnelles.

1.!|="sietseul ementsi |=!$".

2.!/"sietseul ementsi |=!%".

Démonstration.1.Conséquencedirectedupoint4dela Proposition2.22

2.|=!%"ssi3v!Val,v(!%")=1(parladé finition detautologie)ssi3v!Val,v(!)=v(")

(parlatable dev eritéde%)ssi3v!Val,v!mod(!)ssiv!mod(")ssimod(!)=mod(") ssi"/!.

2.3.2La conséquen celogique(d'unensembledeformules)

Lesformule spropositionnellespeuven têtrevuescommedescontraintessurlespro positions atomiques.Parexemple, p"qcontraintpetqàêtrevraies,oùp$qcontraintqàêtrevraietoute foisquepestvraie .Ilestdonctrèscoura ntd econsidé rerdesensemb lesdeformul esproposition- nellespourmodél iserdesproblèmesdesa tisfactiondecontr ai ntes.Unevaluatio nsat isfaisanttoute formuledel'ensemblepour rado ncseconsidérercommeunesolution duproblème. Onéte ndlesdéfinitionsvu esprécé demmentauxensembles deformules. Définition2.26(Modèle).Unmodèled'unensemble deformules!estunev aluati onvtelleque Cetense mbledemodèlesestdoncl'e nsembl edesvaluationsqu'onp eutattrib uerauxvaria bles sionv eutr espectertoutes lescontraintesde!. Définition2.27(Satisfaisabilité/Consistance,Insatisfaisabilité/Contradiction).Unen semblede formules!estquotesdbs_dbs7.pdfusesText_13

[PDF] logique propositionnelle exercice corrigé

[PDF] calcul propositionnel exercices corrigés

[PDF] logique propositionnelle table de vérité

[PDF] calcul propositionnel formel

[PDF] calcul des propositions exercices corrigés

[PDF] le resultat dune multiplication est

[PDF] comment calculer le taux de possession du stock

[PDF] cout de stockage annuel

[PDF] calcul du stock moyen

[PDF] exercice cout de passation et possession

[PDF] calcul tangente formule

[PDF] calcul tangente fonction

[PDF] calcul tangente en ligne

[PDF] calculer tangente calculatrice

[PDF] a quoi sert le sinus