Az ELTE BTK Logika tanszek szeminariuman (a korabban szetkuldott programtol elterve) marcius 19-en (csutortok) du. 4 orakor BIMBO KATALIN tart ket eloadast: 1. "Display Logic" explicit kombinatorokat tartalmazo rendszerekre 2. Dualis kombinatorikus logika Helyszin: Bp. V. Pesti B. u. 1. A ep. felem. 23. A masodik eloadas varhato kezdesi ideje: 1/2 5 Bimbo Katalin ket kapcsolodo publikaciojat keresre ps-filekent megkuldom. Az eloadasok kivonata: 2.Dualis kombinatorikus logika A "klasszikus" kombinatorikus logika rendelkezik ket fontos tulajdonsaggal: "Church-Rosser" (CR), es (2) konzisztens. (1) intuitive azt jelenti, hogy a kombinatorikus logikai redukciot elemi szamolasi lepesnek tekinve, teljesen mindegy, hogy egy terminusban a lepeseket milyen sorrendben tesszuk meg - ugyanazt az eredmenyt kapjuk. (A kombinatorikus logika szamitogepes alkalmazasaiban ez egy igen fontos szempont.) (1) kovetkezmenye (S \not\equiv K-t felteve) (2). A "dualis" kombinatorokat Dunn vezette be (Dunn & Meyer 1997), szubstrukturalis logikak Gentzen-fele szekvens rendszerben valo formalizalasahoz. A dualis kombinatorok egyszeruen a "rendes" kombinatorok tukorkepei, es mint ilyenek onmagukban semmifele erdekes tulajdonsaggal nem rendelkeznek. Amennyiben a szokasos es a dualis kombinatorokat egy rendszeren belul tekintjuk, ugy az ilyen dualis kombinatorikus logika nem ekvivalens a "szokasos" kombinatorikus logikaval. Az eloadasban bizonyitom, hogy a kombinatorikusan teljes dualis kombinatorikus rendszer nem CR es inkonzisztens. Tovabba, bemutatok bizonyos reszeredmenyeket: kombinatorikusan nem teljes bazisok milyen feltetelek mellett CR-ek vagy nem CR-ek, konzisztensek/inkonzisztensek. 1. 'Display Logic' explicit kombinatorokat tartalmazo rendszerekre Meyer 1976 bevezetett egy "altalanositott" Gentzen kalkulust, melyben a strukturalis szabalyokat explicit kombinatorok helyettesitik. Dunn & Meyer l997 tovabbfejlesztette ezt a megkozelitest, a kombinatorokat teljes mertekben formulaknak tekintve; ezekben a rendszerekben a logikai kapcsolok: \circ ("fusion") es \rightarrow. A metszetszabaly megengedese konzervativ (ET). ezekben a rendszerekben. Bimbo & Dunn l998 kibovitette ezeket a rendszereket konjunkcioval es alternacioval (disztributiv es nem-disztributiv modon) es megmutatta, hogy ET igaz. Mindezek a rendszerek szingularisak a jobb oldalon (Curry 1963 terminologiajat hasznalva). Tobb formulat is megengedve a jobb oldalon, felmerul a kerdes, hogy milyen szabalyokkal vezethetjuk itt be a kombinatorokat. Ket termeszetesnek tuno megoldas kinalkozik. Az egyikben a kombinatorokat egyforman vezetjuk be a ket oldalon; ekkor ET hamis fuggetlenul attol, hogy mely kombinatorokrol van szo. Az eloadas a Display Logic (DL) (vo. Belnap 1982) egy olyan valtozatat ismerteti, amelyben explicit kombinatorok vannak a jobb oldalon szingularis rendszerekben. A kombinatorokat, a reflexivitasi axioman tul, "strukturalis szabalyok" is bevezethetik, mint strukturalis konstansokat. Minden ilyen konstanst (szabaly alkalmazassal) formulava tehetunk. Az eloadas illusztralja az ET hamissagat a fent emlitett megkozelitesben es tesz egy megoldasi javaslatot - a strukturalis konstansok formulava alakitasanak a korlatozasat. ============================================================================== Andras Mate CSc, assoc. prof. -- Dept. of Symbolic Logic Lorand Eotvos University Budapest, Faculty of Arts and Humanities H-1364 Budapest, POB 107 Phone: (36 1) 266 9100/5328 -- TAD/Fax: (36 1) 266 41 95 e-mail:mate@isis.elte.hu Home: H-1119 Budapest, Nandorfehervar koz 11 / Phone: (36 1) 204 0489