Formules et sequents Positions Coups Formalisation La theorie de MALL

De
Publié par

Formules et sequents Positions Coups Formalisation La theorie de MALL Mon deuxieme jeu logique: MALL Dedou Janvier 2012

  • deuxieme jeu logique

  • formules mult

  • all en echangeant ?

  • formule

  • famille finie de formules


Publié le : dimanche 1 janvier 2012
Lecture(s) : 11
Tags :
Source : math.unice.fr
Nombre de pages : 24
Voir plus Voir moins
Formulesets´equnestoPisitnoCsuoFopsalrmatisnLio´htairoeMedeLLA
Mon
De´dou
MALL
deuxi`emejeulogique:
Janvier 2012
mrluseteoFsPositios´equentamroasiloCsnFspuor´edeieontithLaAMLL
L’ensembleMALLdes formules mult-additives estd´eniparlagrammaire: M:= x|x|>|0|1|⊥|MM|M&M|MM|MOM.
Les formules mult-additives
Exercice Ecrivez une formule impliquant tous les constructeurs.
ormaupsFtionlisae´roaLhtAMLLeied
Eh bien les quatre constantes correspondent au casI:=pour ces quatreconnecteursavecarit´evariable.
Onachoisided´enirquatreconnecteursbinaires,maisonaurait ´ef´rerintroduirequatreconnecteursdarit´evariable,genre pu pr e
iAi
Comprendre les constantes
nsCoitiosPosuent´sqesetemrluoF
aLhte´roeiedAMLLupsFormalisationtneusoPsoitioCsnFoulrmeteseqs´
Exercice Calculezlane´gationde(>O>)&(0⊗ >).
ne´gation
La
O.
Lane´gation prolongecelledeALLene´changeantet
ionLisatrmalpsFoLALdeMeoeirta´htssequ´eorFlemunoituoCsstneisoP
Un sequent, c’est ´ une famille finie de formules.
Maisleˆ´quentonledessineaussiaveclesformulesa` meme se , gauche
ouavecdesformulesa`gaucheetadroite `
>O0,10,⊥ `
>O0,10,`1
Lesse´quents
Ondessineunse´quentcommec¸a:
`0⊗ >,O>,1
Disonsquunse´quentnormal,cest unse´quentquinadesformulesqu`adroitede`.
Nor lisati de ´ ts ma on s sequen
1O,0`0⊗ >,.
Exercice Normalisezlese´quent
sContisirmFopsoue´steseloPstneuqeMALriedLtaoilasi´hoeLntaFormu
tneusoPsoitioCsnsFupmaorsaliontiFormulesets´eqLLMAdeieor´ethLa
`MF`T.
Exemple
Si Toi et Moi s’affrontent autour de la formuleF onpeutpenserqueMoiveutvaliderlese´quent`Ftandis que Toi veut validerF`. On a quelque chose comme
ToietMoipartagentlesformulesmaislesr´epartissentdansdes s´equentschacuna`safac¸on.
`M1 et tandisqueToiaura`age´rerleseulsequent ´
1,⊥ `T.
apr`esuncoup,Moide´rlesduxse´quents vra gere e
`M
Si on part de la position
`M1⊗ ⊥ `T,
Exemple
oeirdeMeLALrmalisationLath´PositionsCoupsFoumelesste´uqnestorF
Unepr´eposition,cest unefamilledeformulesdeMALLindex´eeparunensembleI fini un ensemble finiGeeMqouieenstssd´(d) un ensemble finiD(e´uqedssTodetseni) deux applicationsg:IGetd:IDsiestnelsquir´epart formulesdanslesse´quents un´ele´menttdeGou deDel`ereirepn)qutokeio(n´tme,el se´quentactif.
Pre´positions
iroeMedeLnoi´htaLALroFsteseluments´equtionPosispoFCsuositamrla
Exemple
Si on part de la position`M1⊗ ⊥ `TtelcevaiToezchinmo´e Toicommenceparpasserlet´emoin`aMoi ensuite Moi ”casse” leuinuqemeio`nlaseast´leeeptr s´equentdeToi
1,⊥ `T.
muleFore´uqesstoPisnestedeMALLontiousCFopsalrmtasiLnoi´htairoe
deMeLALoPisneste´uqesstmuleForiroe´htaLnoitasialrmFopsousConti
conditiondacyclicit´e
La
Uneposition,cestunepre´positionve´riant le graphe ayant
est acyclique (un arbre).
GqDcomme ensemble de sommets Icomme ensemble d’arcs getdcomme source et but
Soyez le premier à déposer un commentaire !

17/1000 caractères maximum.