cours-logique

Description

LogiqueL3 informatique – Universite de la ReunionJ. Diatta et F. Mesnard2Table des matieres1 Systemes formels 5I De nitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5I.A Ensembles recursifs et recursivement enumerables . . . . . 5I.B Systemes formels . . . . . . . . . . . . . . . . . . . . . . . 6II De nitions supplementaires . . . . . . . . . . . . . . . . . . . . . 7III Resultats generaux . . . . . . . . . . . . . . . . . . . . . . . . . . 82 Calcul propositionnel 9I Syntaxe du calcul propositionnel . . . . . . . . . . . . . . . . . . 9II Systeme formel du calcul propositionnel (sfcp). . . . . . . . . . . 10III Semantique du calcul propositionnel . . . . . . . . . . . . . . . . 11III.A De nitions sur l’interpretation semantique des formules . 11III.B Simpli cation de formules de F . . . . . . . . . . . . . . . 12III.C Quelques remarques . . . . . . . . . . . . . . . . . . . . . 12C.1 Negation d’une implication . . . . . . . . . . . . 12C.2 Contraposee, reciproque et inverse . . . . . . . . 13C.3 Equivalence semantique . . . . . . . . . . . . . . 13III.D Quelques resultats . . . . . . . . . . . . . . . . . . . . . . 14III.E Formes conjonctives . . . . . . . . . . . . . . . . . . . . . 14IV Resolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153 Calcul des predicats du premier ordre 17I Syntaxe du calcul des predicats du premier ordre . . . . . . . . . 17I.A Sous-formules ...

Informations

• Publié par: Theyl
• Nombre de lectures: 73
• Langue: Catalan

Extrait

L3

Logique

informatique – Universit´ e

J.

Diatta

et

F.

de

Mesnard

la

R´eunion

2

Tabledesmati`eres

1Syst`emesformels IDe´finitions............................... I.AEnsemblesre´cursifsetre´cursivemente´num´erables..... I.BSyst`emesformels....................... IIDe´finitionssupple´mentaires..................... IIIR´esultatsge´ne´raux.......................... 2 Calcul propositionnel I Syntaxe du calcul propositionnel . . . . . . . . . . . . . . . . . . IISyst`emeformelducalculpropositionnel(sfcp)........... IIIS´emantiqueducalculpropositionnel................ III.ADe´finitionssurl’interpr´etations´emantiquedesformules. III.B Simplification de formules deF. . . . . . . . . . . . . . . III.C Quelques remarques . . . . . . . . . . . . . . . . . . . . . C.1N´egationd’uneimplication............ C.2Contrapos´ee,r´eciproqueetinverse........ C.3 Equivalen ´ ti e . . . ce seman qu . . . . . . . . . . . III.DQuelquesr´esultats...................... III.E Formes conjonctives . . . . . . . . . . . . . . . . . . . . . IVRe´solution............................... 3Calculdespr´edicatsdupremierordre ISyntaxeducalculdespre´dicatsdupremierordre......... I.A Sous-formules d’une formule . . . . . . . . . . . . . . . . . I.BVariableslibresouli´ees................... I.C Standardisation des variables . . . . . . . . . . . . . . . . I.D Substitution d’une variable par un terme . . . . . . . . . IISyste`meformelducalculdespr´edicatsdupremierordre(sfcppo) IIISe´mantiqueducalculdespr´edicatsdupremierordre....... III.ADe´finitionssurl’interpre´tations´emantiquedesformules. IVPre´parationdesformules Mod`elesdeHerbrand......................... IV.AFormepre´nexe........................ IV.B Forme de Skolem . . . . . . . . . . . . . . . . . . . . . . . IV.C Forme clausale . . . . . . . . . . . . . . . . . . . . . . . . IV.DProbl`emedelad´emonstrationautomatique........ IV.EMode`lesdeHerbrand.................... IV.FIllustrationduth´eore`medeHerbrand...........

3

5 5 5 6 7 8 9 9 10 11 11 12 12 12 13 13 14 14 15 17 17 18 19 19 19 20 21 22 23 23 24 25 25 26 27

4

V

VI

` TABLE DES MATIERES

IV.GArbress´emantiques............... Unification . . . . . . . . . . . . . . . . . . . . . . . V.A Substitutions . . . . . . . . . . . . . . . . . . V.B Algorithme d’unification de deux atomesAet Re´solution........................ VI.ASyst`emeformelder´esolutionavecvariables.

. . . . . . B . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

. . . . . .

27 29 29 30 31 31

Chapitre 1

Syst`emesformels

Lathe´oriedesemst`efloersmyssquelnsleutonpeoncunueitste´gerdacadlare´n exprimerete´tudier,defac¸onrigoureuse,lanotiondeme´canismed´eductif.En particulier,lesconceptsdede´monstrationetdeth´eor`emedeviennentdescon- ceptsmath´ematiquesobjets,ausujetdesquelsonpeut´etablirdesr´esultats (qualifi´esdeqieusta´hmetam´etam)uaautats´rselusebatedtilquren´’oemmˆitet sujet des nombres entiers ou des matrices inversibles. Lare´alisationd’unsyst`emeformelfournituncadrederepre´sentationd’une r´ealite´donne´eou`desreglesautomatiquesproduisenttouslese´l´ementsvrais.Le ` butestd’avoirunpetitnombredev´erite´sinitiales(cesontlesaxiomes) et de disposerdeme´canismesderaisonnement(cesontlesefncneredsi’geel`r) pour ´ ´´ledesv´erite´scach´ees. reve r Parexemple,unsyst`emeexpert,quiestconstitu´ed’unebasedefaitsetde `lespttantd’inf´ererdenouvellesconnaissances,estunsyste`meformel. reg erme

IDe´finitions I.AEnsemblesr´ecursifsetr´ecursivement´enum´erables SoitEetFdeux ensembles tels queE⊆Fetxun objet arbitraire deF. Consid´eronsl’assertion“xappraitne`taE” . – L’ensembleEest ditreconnaissableouecr´siurfs’il l’on dispose d’un algo- rithme,aulieud’uncrit`erenonne´cessairementex´ecutable,pourcalculer,quel que soitxvaleurde,laed’lsaes´vretie´rpnoitrtnede´cee. ´ – L’ensembleEsera ditsemi-reconnaissableouecurr´evistnemune´re´mleabs’il existe un algorithme qui, pour toutxtna`appartenaE,e´atlbricaettepropri´et´e enunnombrefinid’e´tapes(maisonn’exigepasquecetalgorithmesetermine lorsquexnsaptse’ntme´eeldeE). ´ Exemple I.1L’ensemble des entiers naturels et l’ensemble des entiers naturels pairssontdesensemblesre´cursifs. Remarque I.1.ntmenu´eerm´leabefis´rtsruceevisTo1)ruce´relbmesnetu 2)Ilexistedesensemblesr´ecursivemente´nume´rablesquinesontpasre´cursifs. 5

` 6CHAPITRE 1. SYSTEMES FORMELS I.BSyst`emesformels On appellesysteme formel(sf)Sdolae´nn:ede ` (a)unalphabetde´nombrableΣ S , (b)unsous-ensembler´ecursifF S de l’ensemble Σ ∗ S desl´´eenemtssetiuinfis’dse deΣ S s,applee´neesbmeledformulesbienforseem´(fbf) deS, (c)unsous-ensembler´ecursifA S ⊆F S eledesbme´nepple,asaxiomesdeS, (d) un ensemble fini Ω S ={r 1 , . . . , r n }defne´ercneeldsdei’r`eg(qui permet- tentd’enrichirlesyste`me)telque,pourchaquer i il existe un algorithme A i uqeeonn´utedurtoi,pof 1 , . . . , f m , f∈F S urlevalalecual,cdev´erit´ede l’assertion“onpeutde´duirelaformuleflesapa`ritrfsedumrof 1 , . . . , f m parlare`gler i itcr´es’:qeiu”c, f 1 , . . . , f m `f. r i Remarque I.2La construction d’un sf illustre bien le processus de definition ´ inductive.Eneffet,e´tantdonn´eunensembleEip-escron(dniti´dfie,sasjbtedo’ tion)parunsch´emad’inductionconsisteentroisphases: - enphase initiale, on choisit unebase ensemble initial d’objets de un, i.e. l’ensemble ; - enphase inductiveo,edelsembunenfinitnd´eorpedselge`rnioctduperme- ttant,`apartird’objetsdel’ensemble,d’enproduiredenouveaux; - enotureclˆephedasd´ec,on’unudiqeatppboejt`entiaremns’ealelbEsi etseulementsionl’obtient`apartird’e´l´ementsdelabaseenenchaıˆnant unnombrefinidere`glesetenproduisant,sinecessaire,desobjetsin-´ term´ediaires. Exemple I.2fomeelrmsyle`esttioSS 1 ap:r´dfiein Σ S 1 ={1,+,=}, F S 1 ={1 n + p n}}1u`o k = 1∙ ∙ ∙1 1 m = 1|, m, p∈N\ {0 | {z } , kfois A S 1 ={1 + 1 = 11}, ` Ω S 1 ={r 1 , r 2 }ou : 1 n + 1 m = 1 p `1 n+1 + 1 m = 1 p+1 r 1 et 1 n + 1 m = 1 p `1 n + 1 m+1 = 1 p+1 . r 2 Remarques I.1ucnd-rapicsnume´hi’dabfpeutˆetred´efin)1’Lneesbmeledfs tion;danscecas,onprendrabiengardedenepasconfondrelesre`glesde productiondecesch´emaetlesr`eglesded’infe´rencedusyste`me. 2)Lesre`glesded’inf´erences’appellentaussire`glesdedontivari´eou ded´noitcude.