Tisztelt Olvas´ok! Jegyzet¨ unk n´egy program haszn´alat´at mutatja be, melyeket m´ agneslemezen is mell´ekel¨ unk. Ezek a ,,matematikai logika” ´es a ,,mesters´eges intelligencia” oktat´as´anak seg´ıt´es´ere alkalmasak. A DEDUCTIO egy sz´am´ıt´og´epes k¨ornyezet, amelyben a felhaszn´ al´ onak mag´anak kell megkonstru´alnia a bizony´ıt´asokat, a program pedig feljegyzi ´es ellen˝orzi azokat. Nagy ´ert´eke ennek a szoftvernek, hogy a levezet´esi rendszert konfigur´alni lehet. A m´asodik r´eszben h´arom automatikus t´etelbizony´ıt´o programot ´ırunk le. Ezek – mind a kvantormentes, mind az els˝ orend˝ u logika eset´en – nagyon gyors keres´esre k´epesek, a leg´ ujabb elm´eleti kutat´asokon alapulva. A matematikai logika oktat´as´aban az elm´eleti alapok megszerz´ese ut´ an nagyon fontos a t´etelbizony´ıt´o k´eszs´eg kialak´ıt´asa. Ezt seg´ıti a DEDUCTIO, m´ıg a mesters´eges intelligenci´aban az automatikus t´etelbizony´ıt´o programok nagyon hasznosak, mivel egyszer˝ u felhaszn´al´oi fel¨ ulet¨ uk r´ev´en nagyon k¨onnyen munk´ara foghat´ok ak´ar bonyolultabb rendszerek logikai komponensek´ent is. A szerz˝ ok
A p´aly´azat elk´esz´ıt´es´ehez a PRO RENOVANDA CULTURA HUN´ ´ GARIAE alap´ıtv´any ,,TUDOMANY AZ OKTATASBAN” szakalap´ıtv´ anya r´eszleges anyagi t´amogat´ast ny´ ujtott.
Lektor: Dr B¨olcskei Andr´as
´ cio ´ Installa
5
´ I. RESZ A jegyzet e r´esz´eben a DEDUCTIO elnevez´es˝ u szoftver haszn´ alat´ ar´ ol tal´ alunk le´ır´ast. Ez a program prec´ız matematikai bizony´ıt´asok konstrual´ ´ as´ahoz ´es m´ar megkonstru´alt bizony´ıt´ asok ellen˝orz´es´ehez ny´ ujt seg´ıts´eget. A program arra szolg´al, hogy 1) a haszn´alt nyelvet ´es az axi´ om´akat r¨ ogz´ıtve, tetsz˝oleges k¨ovetkeztet´est interakt´ıvan levezethess¨ unk a szoftver form´atum´aban, ´ıgy a program form´alis bizony´ıt´asok keres´es´en´el a pap´ırt helyettes´ıti, de intelligens pap´ırt, mert a lejegyz´es folyam´ an ellen˝orzi is a levezet´es korrekts´eg´et; 2) m´ar megtal´alt bizony´ıt´ asokat beg´epelve a program ellen˝orzi azok helyess´eg´et. Ezeken a f˝ oleg az automatikus t´etelbizony´ıt´asban bevethet˝o haszn´alati m´odokon k´ıv¨ ul persze a DEDUCTIO nagyon alkalmas a matematikai logika, ezen bel¨ ul a k¨ ul¨ onb¨ oz˝o levezet´esi kalkulusok begyakorl´as´ara illetve begyakoroltat´as´ara. A DEDUCTIO alkot´oi A. Szmirnov ´es A. Novodvorszkij voltak. Az ´ Oroszorsz´agban, a Moszkvai Allami Egyetemen k´esz¨ ult program angolul kommunik´al a felhaszn´al´oval. A hardver ´es szoftverk¨ ovetelm´enyek: IBM-kompatibilis szem´elyi sz´ am´ıt´ og´ep, 3.0 vagy e feletti verzi´osz´am´ u DOS oper´aci´os rendszer, legal´ abb EGA grafikus k´artya ´es monitor, hajl´ekony- vagy merevlemez (minimum 400 kB). Aj´ anlott hozz´a l´ezerprinter ´es az AMSTEX sz¨ovegform´az´o szoftver a sz´ep kimeneti dokumentumok produk´al´as´ahoz. A DOS-alapokb´ ol a file- ´es k¨onyvt´arstrukt´ ur´at ´es a billenty˝ uzet haszn´alat´at kell ismern¨ unk, valamint – saj´at matematikai-logikai nyelv l´etrehoz´as´ahoz – kell egy sz¨ovegszerkeszt˝o ismerete is. A j´o min˝os´eg˝ u nyomtat´ashoz ismern¨ unk kell az AMSTEX sz¨ovegform´az´o programcsomagot. Matematikai-logikai ismeretek sz¨ uks´egesek. Ezek megszerezhet˝ ok egy egyetemi matematikai logika kurzusb´ol, vagy a k¨ovetkez˝o k¨onyvekb˝ ol: [1], [2], [3].
´ O ´ INSTALLACI A jegyzet lemezmell´eklet´et tegy¨ uk a lemezmeghajt´oba, v´altsunk az A:\DEDUCTIO alk¨onyvt´arba ´es g´epelj¨ uk be: setup. A program megk´erdezi, melyik lemez melyik k¨onyvt´ar´aba install´alja a programot. A SETUP program felm´asolja a program file-ait, ´es egy u ´j file-t is l´etrehoz, DEDUCTIO.CFG n´even.
6
Deductio
A program elind´ıt´ as´ ahoz v´altsunk abba a k¨onyvt´arba, amelybe install´ altuk a programot, ´es g´epelj¨ uk be: deductio.exe. A jegyzet szerz˝oi n´eh´any u ´j p´eldafeladaton k´ıv¨ ul hozz´atettek az eredeti programfile-okhoz egy olyan DEDUCTIO.CFG file-t, amely seg´ıts´eg´evel a programot nem kell install´alni a merevlemezre, hanem az A: meghajt´ o f˝ ok¨onyvt´ar´aban kell kiadni a deductio\deductio parancsot.
´ A MUNKAMENET LE´ IRASA A program els˝o ind´ıt´asakor a program inform´aci´os k´eperny˝oje jelentkezik. Ezt elt¨ untetni a [Space] billenty˝ u megnyom´as´aval lehets´eges. Ezut´ an megjelenik az alapk´eperny˝o, melyet munka k¨ozben ´altal´aban l´ athatunk. Ez k´et ablakra van osztva – a f˝o- ´es az adatbeviteli (input) ablakra; felett¨ uk a st´atuszsor (ahol a men¨ u is megjelenik), k¨ozt¨ uk a munkasor helyezkedik el. A st´atuszsor a rendszer aktu´alis be´all´ıt´asait jelzi ki, valamint azt, hogy [Alt+H]-val mindig helyzet´erz´ekeny seg´ıts´eget lehet k´erni. A f˝oablakot a feladat kijelz´es´ere haszn´aljuk, az input ablakot a formul´ak ´es egy´eb adatok bevitel´ere. Minden ablakb´ol, helyzetb˝ ol az [Esc] gomb n´eh´any megnyom´as´aval ehhez a k´eperny˝oh¨oz lehet eljutni. Itt m´eg egyszer [Esc]-et nyomva pedig a men¨ usor jelentkezik leny´ıl´ o men¨ upontokkal. Egy men¨ upontot eml´ıt¨ unk most: a QUIT parancsot kiadva a programot elhagyhatjuk. A program megjelen´ıt´es´enek r´eszei m´eg a k¨ ul¨onf´ele p´arbesz´edes ablakok. A program haszn´ alat´ anak f˝ obb elemei: els˝o l´ep´esk´ent a feladat (a levezetend˝o k¨ovetkeztet´es) bevitele – azaz a felt´etelek´e (premissz´ ak) ´es a k¨ovetkezm´eny´e (konkl´ uzi´o). Ezeknek a formul´aknak bizonyos nyelviformai k¨ovetelm´enyeknek kell megfelelni¨ uk, viszont a nyelvet viszonylag szabadon konfigur´alhatjuk. M´asodik l´ep´esk´ent a szint´en el˝ore megadott (de szint´en szabadon konfigur´alhat´o) levezet´esi szab´alyok k¨oz¨ ul v´alasztgatva l´ep´esenk´ent le kell vezetni a premissz´akb´ol a konkl´ uzi´ot. Ehhez ismerni kell az adott levezet´esi rendszert. Hogy mi is l´etrehozhassunk u ´j nyelvet ´es sz´am´ara levezet´esi rendszert, el˝obb be kell gyakorolnunk a szoftver munkam´odszer´et; ez´ert aj´anlatos v´egigolvasni e jegyzetet.
ADATBEVITEL Egy feladattal val´o foglalkoz´ashoz persze el˝obb be kell g´epeln¨ unk a feladat sz¨oveg´et. Vegy¨ unk egy egyszer˝ u p´eld´at:
Adatbevitel
7 A ∨ B, A ⊃ C, B ⊃ D ` C ∨ D-t
A f˝omen¨ uben a kurzorvez´erl˝o nyilakkal az UTILITIES/EDIT parancsra ´ allunk ´es [Enter] benyom´as´aval kiv´alasztjuk. Ekkor a kurzor a f˝ o ablakba ker¨ ul. Egyel˝ore csak egy ` jelet tartalmaz´o sort l´athatunk. Ez a k¨ovetkeztet´es jele, ez el´e kell bevinni a premissz´ainkat, s e m¨ og´e a c´elformul´ankat, a konkl´ uzi´ot. Egy sorba maximum egy formula ker¨ ulhet. A ` jel el´e besz´ urhatunk egy sort, ha a sorra ´allva megnyomjuk az [Insert] billenty˝ ut, ´es az input ablakban bebillenty˝ uzz¨ uk a k´ıv´ant formul´ at. Ugyan´ıgy a l´etrej¨ov˝o formul´ak el´e is u ´jabb ´es u ´jabb premissz´akat t˝ uzhet¨ unk be. A premissz´ak sz´ama ak´ar nulla is lehet, ekkor a konkl´ uzi´onak logikai t¨ orv´enynek kell(ene) lennie. A konkl´ uzi´ ot bevinni u ´gy lehet, hogy r´ a´ allunk a kurzorral a ` ut´ani sorra ´es [Space]-t nyomunk. Ugyan´ıgy lehet m´ ar bevitt sort u ´jrag´epelni, jav´ıtani. Ez a k´et t´eny annak a –logik´aban bevett– szok´asnak felel meg, hogy a konkl´ uzi´o is lehet u ¨res, ´es akkor ellentmond´ ast ´ert¨ unk rajta. Sort t¨ or¨ olni a [Delete] gombbal lehet. Az input ablakban bevitt formul´aknak a DEDUCTIO form´ atum´ aban kell l´etrej¨onnie (de ez a form´atum v´altozhat, ha ´atkonfigur´aljuk). Az els˝ o ind´ıt´askor ´es am´ıg nem v´altoztatunk rajta, a term´eszetes levezet´esi rendszer nyelv´et kell haszn´alnunk. Atomi formulak´ent az A,B,C,D,E ´es m´eg n´eh´ any nagybet˝ u ´es maximum n´egy sz´amjeggyel indexelt v´altozatuk j¨ohet sz´ oba, valamint az egyenl˝os´egjel. Logikai ¨osszek¨ot˝ojelk´ent sz´oba j¨ohetnek az & (´es), ∨ (vagy), ⊃ (implik´aci´o), ¬ (nem), ⊥ (hamis) jelek; rendre 2, 2, 2, 1, 0 argumentumsz´ammal, v´eg¨ ul kvantork´ent a ∀ ´es az ∃ jelek. E jeleket az input u ¨zemm´odban az als´o sorban mutatott funkci´obillenty˝ ukkel, ill. ezek [Alt], [Shift] vagy [Ctrl] gombbal val´o kombin´aci´oival lehet bevinni. E jelekre ´erv´enyesek a logik´aban szok´asos precedencia-szab´alyok, egy elt´er´essel: itt A ∨ B ∨ C azt jelenti, hogy A ∨ (B ∨ C). Az input ablakban lehet haszn´alni a kurzorvez´erl˝o nyilakat, a [Home], [End], [Delete], [Backspace] gombokat. A formula hosszabb is lehet egy sorn´al, ekkor a formula mozoghat balra-jobbra. Ha k´esz a formula, [Enter]rel lehet bevinni a f˝o ablakba, ha viszont abba akarjuk hagyni a formula szerkeszt´es´et, [Esc]-el ezt is megtehetj¨ uk. Ha a beg´epelt formula hib´ as, egy hiba¨ uzenettel visszat´er¨ unk az input m´odba. Ha az ¨osszes formul´at bevitt¨ uk, v´eg¨ ul az [Esc] gombbal l´ephet¨ unk ki az adatbevitelb˝ ol.
8
Deductio
´ AZ ELS PELDA 2 3 4 1 5
A bevitt A⊃C B⊃D A∨B ` C ∨D
feladat: premise premise premise
Most k¨ovetkezhet a feladat megold´asa – a levezet´es megkonstru´ al´ asa. Egy p´eld´an kereszt¨ ul mutatjuk be, mik a teend˝oink. T¨obb l´ep´es sz¨ uks´eges – minden l´ep´esben kiv´alasztunk egy levezet´esi szab´alyt, ´es alkalmazzuk a meglev˝o feladatra. Milyen hat´assal vannak ezek az aktu´alis levezet´esre? K´etf´ele alapt´ıpusa van a szab´alyoknak. 1) A szintetikus szab´ aly a meglev˝o feltev´esekhez f˝ uz egy u ´jabbat, amely k¨ ovetkezm´enye az eddigieknek. Tipikus szintetikus szab´aly p´eld´aul: F 1&F 2 ⇒ F 1 vagy & se ⊥ si F ; ¬F ⇒ ⊥. Az els˝o esetben a program keres az aktu´alisan meglev˝o felt´etelek k¨ oz¨ ott F 1&F 2 alak´ ut, ´es ha van, bevezet egy u ´jabb felt´etelt is, F 1-et. Az & se szab´aly nev´eben az & azt jelzi, hogy a szab´aly az & logikai jellel foglalkozik, ,,s” a szab´aly szintetikus volta miatt ´all ott, az ,,e” pedig amiatt, hogy a szab´aly ezt a jelet elimin´alja, azaz kik¨ usz¨ob¨oli. Ennek ellent´ete az ,,i” – introdukci´o, azaz bevezet´es. 2) Az analitikus szab´ aly viszont elemzi a m´ar megl´ev˝o feladatot – a konkl´ uzi´ot is, ez´ert a szab´aly le´ır´as´aban mindig szerepel a ` jel is! –, ´es ha lehet illeszteni az aktu´alis konkl´ uzi´ora ´es a felt´etelek valamelyik´ere, akkor egy vagy t¨obb u ´j feladatot vezet be helyette, rem´elhet˝oleg k¨onnyebben megoldhat´ot. Tipikus k´epvisel˝oje: ⊃ ae F 1 ⊃ F 2 ` F 3 ⇒ ¬F 3 ` F 1/F 2 ` F 3 & ai ` F 1&F 2 ⇒` F 1/ ` F 2. A [Space] gombbal bejutunk a levezet´esi szab´alyok men¨ uj´ebe – belekezdhet¨ unk a levezet´esbe. A szab´alyv´alaszt´o men¨ u fels˝o sor´aban a ,,Natural Deduction” feliratnak kell lennie. A kurzorral a k´ıv´ant szab´alyra ´ allva [Enter]-rel v´ alaszthatunk a szab´alyok neve k¨ozt. A v´alaszt´ast seg´ıti, hogy a munkasorban megjelenik a szab´aly le´ır´asa. V´alasszuk a ∨ ae-szab´ alyt. Ekkor a munkasorban felt˝ unik a szab´aly le´ır´asa
˝ pe ´lda Az elso
9
F 1 ∨ F 2 ` F 3 ⇒ F 1 ` F 3/F 2 ` F 3, az F 1 ∨ F 2 piros alapon feh´er bet˝ ukkel ´ırva. Meg kell adnunk, melyik sort gondoltuk F 1∨F 2 szerep´eben. A kurzorral ´alljunk r´a a 4. sorra (A∨B)! Ha j´ o form´aj´ u soron ´allva nyomjuk meg a [Space]-t, elfogadja, ha rosszon, nem csin´al semmit, ha m´egis ink´abb m´as szab´ alyt akarunk alkalmazni: [Esc]-et nyomjunk. Ha a 4. sz´ am´ u A ∨ B formul´ara ´alltunk r´a, elfogadja, ´es ha maradt volna m´eg k´erd´eses hely, azt is hasonl´oan kellett volna megadnunk (most nincs t¨obb k´erd´eses hely). Ha az ¨osszes feltett k´erd´est megv´ alaszoltuk (azaz az ¨osszes piros alap´ u absztrakt formula s´arg´aval van ´ırva), akkor [Enter]-t nyomva a program v´egrehajtja a szab´alyt. 2 3 4 6 9 7 8 1 12 10 11 5
A⊃C B⊃D A∨B →? | A | ` | C ∨D →? | B | ` | C ∨D C ∨D
premise premise premise assumption
assumption
∨e ; 4, 9-8, 12-11
T¨obb u ´j sor is megjelent. Az eredeti ` jel, az 1. sor elt˝ unt. Ehelyett k´et u ´j ` jelent meg a k´et u ´j al´arendelt lemm´aban. L´athatjuk az els˝ o lemma bel´ep´esi pontj´at (6. sor) (→? ), a lemma lok´alis feltev´es´et (9. sor), a lok´ alis ` jelet (7. sor) ´es a lemma konkl´ uzi´oj´at (8. sor). Felismerhet˝ok a m´ asodik u ´jonnan bevezetett lemma hasonl´o r´eszei is. Mindk´et lemma formul´ ai egyegy von´ask´aval vannak jel¨olve. L´epj¨ unk be az els˝o lemm´aba, a bel´ep´esi pontj´an az [Insert] gombot nyomva (6. sor). 2 A ⊃ C premise 3 B ⊃ D premise 4 A ∨ B premise 6 →? 9 A assumption 7 | `
10
Deductio
8 | C ∨D 1 →? 12 | B assumption 10 | ` 11 | C ∨ D 5 C ∨D ∨ e; 4, 9-8, 12-11 Eddig a f˝o feladat szintje volt aktu´alis, most viszont a lemma, ez´ert az ehhez tartoz´o von´ask´ak most kis t´eglalapok alakj´aban jelennek meg. Ilyenkor a lemma saj´at felt´etelei mellett persze a k¨ uls˝o szint felt´etelei is haszn´alhat´ok, m´ıg aktu´ alis konkl´ uzi´onak a lemma konkl´ uzi´oja sz´am´ıt. V´alasszuk az ⊃ se szab´alyt, a 2. sor legyen F 1 ⊃ F 2, a 9. sor pedig F1, ´ıgy nyerj¨ uk ugyanebben a lemm´aban u ´j felt´etel¨ ul C-t. M´eg egy szintetikus szab´allyal, a ∨ si-val vezess¨ uk be u ´j hipot´ezisk´ent C∨D-t. Ehhez azonban az F 1-re val´o r´ amutat´as ut´an nem megmutatni, hanem beg´epelni kell F 2-t, az input ablakban. Ez az´ert van, mert ez olyan szab´aly, melyn´el nem biztos, hogy egy, a feladat formul´ai k¨oz¨ott m´ar szerepelt formul´ at akarunk haszn´alni. Ha beg´epelt¨ uk D-t ´es [Enter]-t nyomunk, a szab´ aly sz´epen v´egrehajt´odik. Az els˝o lemm´at kipip´alhatjuk – a DEDUCTIO ,,→ +” jel´evel –, ugyanis a felt´etelek k¨oz¨ott megjelent a konkl´ uzi´o. Levezet´est mindig ´ıgy lehet lez´arni, ha nem vezetj¨ uk vissza m´as feladatokra. 2 A⊃C premise 3 B⊃D premise 4 A∨B premise 6 →+ 9 A assumption 13 | C ⊃ e; 2, 9 8 | C ∨ D ∨ i 1; 13 1 →? 12 | B assumption 10 | ` 11 | C ∨ D 5 C ∨D ∨ e; 4, 9-8, 12-11 Hasonl´o u ´ton a m´asodik lemm´at is bebizony´ıthatjuk. Ha az ¨ osszes ` jel elt˝ unt, a ,,Deduction is ready” feliratot kapjuk: a feladat k´esz. [Esc]-el kil´epve a men¨ ube az UTILITIES/CLEAR parancsot kiadva u ´j feladatba kezdhet¨ unk.
´sek megjelen´ıte ´si mo ´ dja A levezete 2 3 4 6 9 13 8 1 12 14 11 5
A⊃C B⊃D A∨B →+ | A | C | C ∨D →+ | B | D | C ∨D C ∨D
11
premise premise premise assumption ⊃ e; 2, 9 ∨ i 1; 13 assumption ⊃ e; 3, 12 ∨ i 2; 14 ∨ e; 4, 9-8, 12-11
´ ´ ´ A LEVEZETESEK MEGJELEN´ ITESI MODJA Meg kell ismern¨ unk a DEDUCTIO-beli levezet´esek k´eperny˝ on val´ o megjelen´ıt´es´enek jel¨ol´esi rendszer´et, hogy k¨ovetni ´es l´etrehozni tudjunk levezet´eseket. A levezet´es szerkezet´enek alapja az al´ arendelt levezet´esek fogalma: az adott k¨ovetkeztet´est u ´gy vezetj¨ uk le, hogy visszavezetj¨ uk n´eh´ any seg´edt´etelre (lemma). A lemm´aknak azt´an u ´jabb lemm´ai lehetnek ´es ´ıgy tov´abb. Hogy ´atl´athassuk a szitu´aci´ot, – mely ilyen egym´asba ´agyaz´ od´ asok r´ev´en bonyolultt´a is v´alhat – a lemm´ak be´agyaz´od´as´anak m´elys´eg´et a lemma formul´ai el˝ott ´all´o von´ask´ak sz´ama jelzi (|). Az eredeti feladat a 0 szinten all, el˝otte egy (|) sem ´all. Ezekb˝ol lehet leolvasni a levezet´es elrendez´es´et. ´ A lemm´ak egym´asba ´agyaz´od´as´at egy fa alak´ u gr´afk´ent lehet elk´epzelni. Az eredeti feladat ´all a 0 szinten, az a fa t¨orzse. Egy cs´ ucs ´again a bel˝ ole sz´ armaz´o lemm´ak ´allnak, a fa v´eg´en, a levelekben pedig a m´eg nyitott (m´eg bebizony´ıtand´o →?) vagy m´ar lez´art lemm´ak (→+). Az alap´ertelmezett teljes n´ezeti m´odban a levezet´es teljes r´eszletess´eggel l´athat´o. Ez a [Ctrl+F], ,,Full” v´alaszt´ assal k´erhet˝o. A lemm´ak szerkezet´et a [Ctrl+G]-,,Graph” n´ezeti m´oddal vizualiz´alhatjuk. Ilyenkor a lemm´ aknak csak a helye l´athat´o. A [Ctrl+S]-sel v´alaszthat´o ,,Short” n´ezeti m´ od r´eszletess´egben e kett˝o k¨oz¨ott ´all: itt csak az aktu´alis lemma felt´etelei ´es konkl´ uzi´oja l´atszik. A n´ezeti m´odot az OPTIONS/VIEW men¨ upontban is ki lehet v´alasztani. A feladat megold´asa sor´an mindig van egy aktu´alis lemma, amelynek
12
Deductio
konkl´ uzi´oja jelenti az aktu´alis r´eszc´elt. A c´el el´er´ese form´alisan a ` jel elt¨ untet´es´evel egyen´ert´ek˝ u – ez akkor t¨ort´enik, ha a lemm´at visszavezetj¨ uk al´ arendelt lemm´akra, vagy ha siker¨ ul egy, a konkl´ uzi´oval egybees˝o felt´etelt elnyerni –, ez esetben k´esz az aktu´alis levezet´es. Ilyenkor az eredeti levezet´esben elt˝ unik a ` jel, m´ıg a bevezetett lemm´akban felt˝ unik. A lemm´ ak kezdete a →? jelsorozattal van megjel¨olve, ezt nevezz¨ uk a lemma bel´ep´esi pontj´anak. Ha a lemm´at lez´artuk, azaz siker¨ ult a konkl´ uzi´ot megkapnunk, akkor a lemma bel´ep´esi pont →+ jelre v´alt. Az aktu´alis lemm´ab´ol megold´as vagy m´as lemm´akra val´o visszavezet´es n´elk¨ ul a [Delete] gombbal lehet kil´epni. A lemm´aba, hogy foglalkozhassunk vele, be kell l´epni, a bel´ep´esi soron benyomva az [Insert] gombot. A lemma lok´ alis felt´eteleit ekkort´ol kezdve haszn´alhatjuk. Persze az aktu´alis lemma bizony´ıt´as´an´al haszn´alhatjuk a k¨ uls˝obb szintek feltev´eseit. A levezet´esben az ¨osszes formula mellett elolvashatjuk, hogy ker¨ ult a levezet´esbe: a ,,premise” az eredeti feladat premissz´ait, az ,,assumption” a lemm´ak lok´alis feltev´eseit jel¨oli. A konkl´ uzi´ok mellett, am´ıg meg nem kaptuk ˝oket, semmi nem ´all, a megkapott konkl´ uzi´ok ´es a szintetikus szab´allyal megkapott felt´etelek mellett meg az ´all ott, melyik levezet´esi szab´allyal keletkezett mely formul´a(k)b´ol.
´ ´ LEVEZETESI SZABALYOK A program els˝o ind´ıt´asakor a term´eszetes levezet´esi rendszer van be´ all´ıtva. (Ha m´egsem ez volna, ´es az al´abb le´ırtakban valami baj mutatkozna, a men¨ u LOGIC pontj´aban a NEC.DED [Natural deduction] be´all´ıt´ ast v´ alasszuk!) Mi ennek a p´eld´aj´an fogjuk tanulm´anyozni a levezet´esi szab´ alyok tulajdons´agait, el˝osz¨or a kvantormentes logika p´eld´ain. 1) Azokat a levezet´esi szab´alyokat, amelyek az aktu´alis feladatot n´eh´ any m´asik feladat megold´as´ara vezetik vissza, analitikus szab´ alynak nevezz¨ uk. P´elda: F 1 ∨ F 2 ` F 3 ⇒ F 1 ` F 3/F 2 ` F 3 Itt az F 1, F 2, F 3 absztrakt formul´ak, ezeket formul´aknak kell megfeleltetn¨ unk. Minden levezet´esi szab´alyban el˝ofordul a ⇒ jel. Azt jel¨oli, hogy ha az aktu´alis levezet´esben szerepel F 1 ∨ F 2 alak´ u felt´etel ´es F 3 alak´ u konkl´ uzi´ o (a konkl´ uzi´ora vonatkoz´o felt´etel jelen esetben semmit nem jelent), akkor az aktu´alis levezet´est vissza lehet vezetni k´et m´asikra. Az els˝oben F 1 ´ all
´si Szaba ´ lyok Levezete
13
lok´ alis feltev´esk´ent, a m´asodikban F 2. A lok´alis konkl´ uzi´o mindk´et esetben F 3 lesz. Analitikusnak nevezik az ilyen fajta szab´alyokat amiatt, hogy analiz´alja, r´eszekre bontja az eredeti feladatot. A m´asik szab´alyfajta az u ´n. szintetikus szab´ aly. P´eld´aul: F1 ⇒ F1 ∨ F2 Az ilyen szab´alyok nem tartalmaznak ` jelet – ez azt jelzi, hogy a szab´ aly nem vezet be u ´j lemm´at, hanem az eddig meglev˝o felt´etelekb˝ol gy´ artunk u ´jabb felt´eteleket. A szintetikus szab´aly az aktu´alis lemm´aba besz´ ur egy u ´jabb felt´etelt, de egy´ebk´ent u ´j lemm´at nem vezet be, azaz a levezet´es f´ aja nem v´altozik. A harmadik fajta, u ´n. glob´ alis helyettes´ıt´es, amelyr˝ol majd a kvantoros szab´alyokn´al fogunk t´argyalni. 2) M´as szempontb´ol is oszt´alyozzuk a szab´alyokat: az elimin´ aci´ os szab´ alyok egy logikai jelet k¨ usz¨ob¨olnek ki (elimin´alnak), az introdukci´ os szab´ alyok egy logikai jelet vezetnek be (introdukci´o). A szintetikus elimin´ aci´ os szab´alyok adott f˝ o logikai jel˝ u felt´etelt felhaszn´ alva produk´alnak u ´jabb felt´etelt (amely szerencs´es esetben m´ar feleslegess´e teszi az eredeti felt´etel haszn´ alat´at), p´eld´aul: & se 1 ⊃ se
F 1&F 2 ⇒ F 2 F 1 ⊃ F 2; F 1 ⇒ F 2
Itt az adott logikai jel˝ u felt´etelt haszn´altuk f¨ol u ´jabb felt´etel produk´ al´ as´ ara. Szintetikus introdukci´ os szab´aly az, amely adott logikai f˝o jellel rendelkez˝ o felt´etelt vezet be meglev˝o felt´etelekb˝ol. P´eld´aul: & si ⊥ si
F 1; F 2 ⇒ F 1&F 2 ¬F ; F ⇒ ⊥
Az analitikus elimin´ aci´ os szab´aly, ha a ⇒ baloldal´at tudja illeszteni az aktu´alis levezet´esre, helyette bevezet n´eh´any al´arendelt levezet´est. Itt az adott logikai jelnek a felt´etelek k¨oz¨ott kellett szerepelnie, m´ıg az analitikus introdukci´ os szab´alyn´al az adott logikai jelnek a konkl´ uzi´ oban kell szerepelnie. ⊃ ae ¬ ae 2 ⊃ ai
F 1 ⊃ F 2 ` F 3 ⇒ ¬F 3 ` F 1/F 2 ` F 3 ¬F ` ⊥ ⇒` F ` F1 ⊃ F2 ⇒ F1 ` F2
14
Deductio ∨ ae
` F 1 ∨ F 2 ⇒ ¬F 1; ¬F 2 ` ⊥
´ MENTESE ´ A LEVEZETES A k´esz levezet´est, de annak b´armely ´allapot´at is t´arolni lehet az UTILITIES/SAVE men¨ uponttal. ´Igy p´eld´aul a munk´ankat fel tudjuk f¨ uggeszteni, ´es m´askor el˝ovenni, vagy a k´esz levezet´est u ´jra megszeml´elni. A SAVE parancs felk´ın´al egy el˝ofelt´etelezett nevet, de ´erdemes ink´ abb valami besz´edes file-nevet v´alasztani. Az aj´anlott kiterjeszt´es: *.prt. Az UTILITIES/LOAD parancs az ´ıgy kimentett levezet´es megszeml´el´es´et – vagy nem k´esz esetben – folytat´as´at teszi lehet˝ov´e. A p´arbesz´edes ablak k´eri a bet¨oltend˝o protokoll-file-n´ev beg´epel´es´et, vagy ha egy *-ot tartalmaz´ o file-nevet adunk meg, ad egy list´at, amelyb˝ol v´alasztani lehet a m´ar l´etez˝ ok k¨ oz¨ ul. Ha nem csak a levezet´es eredm´eny´et akarjuk t´arolni, hanem az odavezet˝o u ´t egyes l´ep´eseit is, akkor a feladat bevitele ut´an, a megold´ as megkezd´ese el˝ott ki kell adni a PROTOCOL/START PROTOCOL parancsot, ´es meg kell adni egy file-nevet. Megjelenik a st´atuszsoron a Prot. Wr. felirat (write). Ilyenkor a levezet´es b´armely pillanat´ahoz megjegyz´est f˝ uzhet¨ unk a PROTOCOL/SET BREAK paranccsal. Ha a megold´as megvan, a v´eg´en nem szabad SAVE parancsot kiadni ugyanarra a protokoll-n´evre, mert az csak a k´esz levezet´est t´aroln´a el, hanem a PROTOCOL/STOP PROTOCOL parancsot adjuk ki. Az ´ıgy elmentett protokoll bet¨ olt´esekor megk´erdezi a program, akarjuk-e a feladat (data) ut´an a protokollt is bet¨olteni. N (nem) v´alasz eset´en nek¨ unk kell levezetni a feladatot, ´am, ha Y-t (igen) adunk meg, a szoftver k´eszen all a levezet´esi l´ep´esek beolvas´as´ara. Ilyenkor [Esc]-et nyomva kisz´ ´ allunk a tov´abbi olvas´asb´ol, ´es esetleg mi fejezhetj¨ uk be a levezet´est; [Space]-t nyomva egy l´ep´es v´egrehajt´odik, ´es a program angolul ki is ´ırja, mit csin´ al; v´eg¨ ul pedig [Enter]-t nyomva a k¨ovetkez˝o megjegyz´esig ugorhatunk. Ezen ismeretek seg´ıts´eg´evel meg lehet vizsg´alni a program szerz˝ oje ´ altal k´esz´ıtett p´eldaprogramokat. Egyel˝ore az EXM01.PRT ´es az EXM02.PRT file-okat n´ezhetj¨ uk ´at. Gyakorl´ask´ent mi is pr´ob´aljunk n´eh´any levezet´est elk´esz´ıteni, menteni, majd protokollal menteni s k´es˝obb u ´jra ´ atn´ezni! P´eld´ak: A, (A&¬C) ⊃ B ` B ∨ C A ∨ B ∨ C ` (A ∨ B) ∨ C ¬(A ⊃ B) ` A&¬B
´ lata A kvantorok haszna
15
´ A KVANTOROK HASZNALATA Ha kvantorokat is haszn´alunk (azaz v´altoz´okat ´es els˝orend˝ u logik´ at), akkor n´eh´any u ´j fogalommal is meg kell ismerkedn¨ unk. Ilyenkor a predik´ atumjelek ut´an (postfix jel¨ol´esm´odban, ill. el˝ott, prefixben) v´altoz´ okat is ´ırhatunk – alap´ertelmez´esben x,y,z,v-t. Lehetnek f¨ uggv´enyjelek (f,g,+,–) is. A formul´ak el´e kvantorokat is tehet¨ unk, ∀xA, ∃xA form´aban. P´eld´ aul: ∀x(∃yB(x, y) ⊃ ∃zC(z, x)). Interpret´aci´ojuk a szok´asos. Tov´ abbra is a term´eszetes levezet´est haszn´aljuk. Tempor´ alis v´ altoz´ onak nevezz¨ uk az olyan v´altoz´ot (,,t” fogja jel¨ olni), amelyet az eredeti feladat megad´asakor nem haszn´alhatunk, de a megold´ as k¨ ozben bevezethetj¨ uk. Minden el˝ofordul´askor u ´j indexet kap. A tempor´ alis f¨ uggv´eny olyan f¨ uggv´enyjel, melyet az eredeti feladat megad´ asakor nem haszn´alhatunk, de a megold´as k¨ozben bevezethet¨ unk. A term´eszetes levezet´esn´el w-vel jel¨olj¨ uk, minden el˝ofordul´askor u ´j sz´ amot kap index¨ ul. A kvantorokr´ol sz´ol´ o levezet´esi szab´alyok a k¨ovetkez˝ok. • • • • • •
∀ ai ∀ se ∃ ai ∃ si ∃ se Globsubst
` ∀vF ⇒` S v, w F ∀vF ⇒ S v, t F ` ∃vF ⇒ ¬∃vF ` S v, t F F ⇒ ∃vS T, v F ∃vF ⇒ S v, w F
A szab´alyokat a rendszer ugyan´ ugy alkalmazza, mint a kvantormentes esetben, hozz´at´eve, hogy S v,w F azt a formul´at jelenti, amelyet F-b˝ ol kapunk a v v´altoz´o hely´ebe w tempor´alis f¨ uggv´enyt ´ırva, mely param´eterei¨ ul F param´etereit kapja; S v,t F azt a formul´at jelenti, melyet F-b˝ ol v v´ altoz´o hely´ere a t tempor´alis v´altoz´ot ´ırva kapunk; v´eg¨ ul S T,v F azt a formul´at jelenti, melyet F-b˝ol a T term hely´ebe a v v´altoz´ot helyettes´ıtve kapunk. Persze ezek alkalmaz´as´ara utas´ıtva a programot, mindig r´ ak´erdez, mutassunk r´a F-re, illetve g´epelj¨ uk v,w,T-t. Az ∃ si szab´ aly eset´en a kurzorral F-ben mozogva, [Space]-szel v´alasztva m´eg azt is meg kell mutatnunk, konkr´etan T mely el˝ofordul´asait kell helyettes´ıteni. A t¨ obbi szab´alyn´al az ¨osszes el˝ofordul´as helyettes´ıt˝odik. A Globsubst szab´aly glob´alis helyettes´ıt´est jelent, azaz olyan helyettes´ıt´est, ahol a levezet´es tempor´alis v´altoz´oit szimult´an az eg´esz levezet´esben
16
Deductio
helyettes´ıteni lehet. Egy p´arbesz´edes ablakban k´er minket a program arra, g´epelj¨ uk be, hogy a tempor´alis v´altoz´ok hely´ebe milyen termet helyettes´ıts¨ unk. [Space]-szel azt a tempor´alis v´altoz´ot v´alaszthatjuk, melyen a kurzor ´all, szerkeszt´es ut´ an [Enter]-rel beolvassa. Ha az ¨osszes helyettes´ıt´est beg´epelt¨ uk, [Esc]-el v´egrehajthatjuk. Az u ´j termek tartalmazhatj´ ak a jelenlev˝o tempor´alis v´altoz´okat ´es f¨ uggv´enyeket is. A helyettes´ıt´es szimult´an: pl. a (t1→t2, t2→t1) helyettes´ıt´es eredm´enye t1 ´es t2 cser´eje lesz. L´athat´o, hogy a tempor´ alis v´ altoz´ ok haszn´ alata azokban a szab´ alyokban fordul el˝o, amelyeknek szok´asos megfelel˝oj´en´el tetsz˝oleges termet lehet v´ alasztani – ezen termek kiv´alaszt´as´at halasztja el k´es˝obbi id˝ opontra a tempor´alis v´altoz´ok haszn´alata. Mikor m´ar l´atjuk, melyik termet lesz j´ o haszn´alni, a Globsubst szab´aly beteszi a k´ıv´ant termet a levezet´esbe. A tempor´alis f¨ uggv´enyeket haszn´al´o szab´alyok pedig k¨or¨ ulbel¨ ul megfelelnek a teljesen u ´j param´etereket haszn´al´o szokott szab´alyoknak (pl. F ` A(x/y) ⇒ F ` ∀xA, ahol y nem param´eter F-ben ´es A-ban). A tempor´alis v´altoz´ok ´es f¨ uggv´enyek haszn´alata egy´ebk´ent az -termet haszn´al´o levezet´esi technik´anak felel meg. L´asd [4].
´ ALIAS NEVEK HASZNALATA K¨oznyelvi form´aban adott feladatokat is meg lehet oldani a DEDUCTIO-val. T¨olts¨ uk be az EXM03.PRT protokollt. Az UTILITIES/ALIASES/LOAD parancs k´erd´es´ere adjuk az EXM03 E.ALI v´alaszt. Ekkor bet¨ olt˝ odnek az A,B,C,D,E predik´atumokhoz megadott k¨oznyelvi mondatok. A logikai jelekhez is rendelhet¨ unk olvasatot. Az UTILITIES/ALIASES/ VIEW paranccsal vagy a [Ctrl+A] billenty˝ ukombin´aci´oval ´atv´althatunk (s azt´ an ugyan´ıgy vissza onnan) a k¨oznyelvi megjelen´ıt´esi m´odra. Sajnos a levezet´es maga nem folyhat ezen a besz´edesebb nyelven, ugyanis a levezet´esi szab´alyok alkalmaz´asa sor´an mindig visszakapcsolunk a logikai jel¨ ol´esre. Mi magunk is l´etrehozhatunk alias neveket, p´eld´aul hozzunk l´etre az EXM03.PRT feladathoz magyar alias neveket! Ezt az UTILITIES/ALIASES/EDIT utas´ıt´as ut´an tehetj¨ uk meg, ahol is be kell g´epelni a logikai jelet ´es a megfelel˝o alias nevet – mindig az [Insert] benyom´asa ut´an. Ha k´esz vagyunk, [Esc]-el elfogadtatjuk. A l´etrehozott neveket menteni lehet: ALIASES/SAVE paranccsal, ill. ´erv´enytelen´ıteni az UTILITIES/ALIASES/
´ ltata ´ sok Automatikus szolga
17
CLEAR-rel, v´eg¨ ul az eddig beolvasott defin´ıci´okat meg˝orizve u ´jakat f˝ uzhet¨ unk hozz´ajuk az .../ALIASES/MERGE paranccsal. A jegyzethez mell´ekelt hajl´ekonylemezen van az EXM03 H.ALI ´es az EXM06 H.ALI file, mely magyar alias neveket haszn´al. Az EXM06.ALI oroszul, az EXM06 E.ALI angolul ,,besz´el”.
´ ´ AUTOMATIKUS SZOLGALTAT ASOK Ezek a levezet´es konstru´al´as´at seg´ıtik. 1) A szab´ alyok sz˝ ur´ese (filterez´es) Ennek bekapcsol´asakor (a OPTIONS/FILTER1 men¨ upont) a ,,Filter1” felirat st´atuszsorban val´o megjelen´ese mellett annyi v´altozik, hogy a levezet´esi szab´alyok k¨oz¨ ul v´alaszt´ ast k´ın´al´o ablakban csak azokat a szab´alyokat lehet v´ alasztani, melyek els˝o absztrakt formul´ajak´ent szerepelhet az a formula, melyen a f˝oablakbeli kurzor ´all. Ez persze m´eg nem garant´alja, hogy a szab´aly t¨obbi r´esz´ehez biztosan tal´alunk illeszthet˝o formul´at a levezet´esb˝ ol. 2) Minimaliz´ aci´ o Ez a szolg´altat´as a levezet´es ´atl´athat´os´ag´at jav´ıtja. Az UTILITIES/MINIMIZE paranccsal egyszer hajthat´o v´egre, m´ıg az OPTIONS/AUTO MINIMIZE folytonoss´a teszi. Vegy¨ uk p´eld´aul az EXM05.PRT protokollt, ´es olvassuk be v´egig az el˝ore adott bizony´ıt´asi protokollt is. L´athat´ o, hogy a 3. sor lemm´ aja (a 3. sort´ol a 4. sorig) nem tartalmaz u ´j feltev´est, ez´ert e lemma lok´alis konkl´ uzi´oja a lemm´an egy szinttel kijjebb is bizony´ıthat´ o. Ilyenkor ezt a lemm´at megsz¨ unteti a minimaliz´al´as, mint feleslegest. Ezenk´ıv¨ ul az olyan formul´akat is kit¨orli a k´esz levezet´esb˝ol, melyekt˝ol a v´egs˝ o konkl´ uzi´o nem f¨ ugg. 3) Generaliz´ aci´ o Ez a szolg´altat´as az OPTIONS/GENERALIZATION paranccsal ´ all´ıthat´ o munk´aba. En´elk¨ ul a levezet´esi szab´alyok a lok´alis felt´eteleket mindig az aktu´alis lemm´aba teszik, generaliz´aci´oval viszont a lehet˝o legk¨ uls˝obb szintre. Ennek f˝oleg a szintetikus szab´alyokn´al l´atjuk nagy haszn´at- p´eld´ anak n´ezz¨ uk meg az EXM08.PRT protokollt. A megold´as sor´an bekapcsolva a generaliz´aci´ot, sokkal gyorsabban megy, mint a PELDA13.PRT-ben, ahol nem haszn´altuk - egy bizonyos r´eszt ott ´eppen a generaliz´aci´o hi´anya miatt k´etszer kellett megcsin´alnunk.
18
Deductio
4) Unifik´ aci´ o Bekapcsolni az OPTIONS/UNIFICATION paranccsal lehet. A kvantoros formul´ak haszn´alat´an´al j¨ohet sz´oba. Nem ugyanaz, mint a rezol´ uci´ oelm´elet unifik´aci´oja; de k´epes arra, hogy ha l´etezik a levezet´est vagy legal´ abb az aktu´alis lemm´at lez´ar´o glob´alis helyettes´ıt´es, akkor a Globsubst szab´ aly alkalmaz´asa eset´en azt megtal´alja. Ha csak az aktu´alis szintet tudja lez´ arni, miel˝ott megtenn´e, r´ak´erdez, hogy megteheti-e, ugyanis az egyik lemm´ aban sikerre vezet˝ o helyettes´ıtes a levezet´es m´ as r´eszeit v´egleg lez´arhatatlann´ a teheti – ezt nek¨ unk kell megfontolnunk. A keres´es nagyon hossz´ u is lehet idej´et tekintve. Az EXM06.PRT ´es az EXM07.PRT file-ok olyan p´eld´ akat tartalmaznak, ahol a glob´alis helyettes´ıt´est automatikusan tal´alta a program. A PELDA21.PRT-ben az EXM07 levezet´ese tal´alhat´o, plusz egy t¨ or´espont egy fontos komment´arral az unifik´aci´ot illet˝oen. Az unifik´ aci´ ot keres˝o algoritmusr´ol b˝ovebben olvashat´o a [5] munk´aban.
´ LOGIKAI RENDSZEREK MAS B´ar a DEDUCTIO al´arendelt lemm´as levezet´es-szerkezete a term´eszetes levezet´esb˝ol sz´armazik, nagyon sok m´as levezet´esi rendszer is – alkalmas megfogalmaz´asban – szint´en megfogalmazhat´o. A programhoz mell´ekelve is tal´ alunk m´eg n´eh´anyat. Persze b´armelyik¨ uk gyakorl´as´ahoz ismern¨ unk kell az illet˝o logikai kalkulust. A LOGIC men¨ u k´ın´alja a v´alaszt´ekot. P´eld´aul az analitikus (m´ as n´even szemantikus) tabl´ o m´ odszer is reprezent´alhat´o: itt ANALTAB n´even szerepel. A LOGIC men¨ uparancsot kiadva r¨ovid le´ır´ast kapunk egy ablakban a v´alaszthat´o rendszerekr˝ ol – ´es a kurzorral v´alaszthatunk. Ez a m´odszer alapvet˝oen c´afol´o m´ odszer: a premissz´ak ´es a konkl´ uzi´o neg´altj´at c´afolva viszont k¨ovetkeztet´eseket is levezethet¨ unk vele. Ez a m´odszer mindig a felt´eteleket vizsg´alja, analiz´ alja, bontja sz´et – ´ıgy nem csoda, hogy itt szinte az ¨osszes szab´aly szintetikus elimin´aci´o, ´es a h´arom analitikus elimin´aci´o is mind a felt´eteleket bontja (csak lemmael´agaz´ast is csin´al), ´es csup´an egy introdukci´os szab´ aly van, uzi´o neg´ altj´ anak a ⊥ ai, amely megfelel a levezet´es kezdet´en a konkl´ felt´etelk´ent val´o bevezet´es´enek: ` F ⇒ ¬F ` ⊥, ´es innent˝ol mehet a tabl´om´odszern´el szok´asos c´afol´o munka. Enn´el a met´ odusn´al a szab´alyok filterez´ese k´ezenfogva vezeti a felhaszn´al´ot a megold´ ashoz. P´elda: EXM04.PRT ´es ugyanez a feladat az ANALTAB levezet´esi
´ s logikai rendszerek Ma
19
technik´aval EXM04A.PRT – itt ki kell pr´ob´alni a filterez´est! Vigy´ azat, ha egy protokollt a DEDUCTIO figyelmeztet´ese ellen´ere nem a saj´ at logikai rendszer´enek ´erv´enye mellett olvasunk be, u ´gy a program lefagyhat! A tabl´o m´odszer megismer´es´ehez aj´anljuk a [3] k¨onyvet. A klasszikus axiomatikus kalkulus is reprezent´alva van az AXIOM.DED file-ban. Ez a minden bevezet˝o logikai kurzusban t´argyalt rendszert jelenti, amelyben ismert dolog, hogy csak nagyon k¨or¨ ulm´enyesen lehet levezet´eseket konstru´alni. Az axi´om´ akat egyszer˝ uen ⇒ F alak´ u szab´alyok seg´ıts´eg´evel bevezethetj¨ uk, ´es a modus ponens ´es m´asik k´et szokott levezet´esi szab´ aly seg´ıts´eg´evel k¨ovetkeztethet¨ unk. A logikai algebra (Boole-algebra) axi´om´aival ´es szab´alyaival kvantormentes formul´akat nagyon k¨onnyen le tudunk vezetni. Az ALGLOG.DED ennek a le´ır´ as´at tartalmazza. Sajnos, a szab´alyok k¨oz¨ott nincsenek ott a ¬-ra ´es az ⊃-re vonatkoz´o t¨orv´enyek, ´ıgy kev´ess´e haszn´alhat´o ez a rendszer. A t¨obbi v´alaszthat´ o *.DED nyelv- ´es levezet´esle´ır´o file m´ar nem m´ as t´ıpus´ u logikai rendszert ´ır le, hanem valamely logikai rendszert b˝ ov´ıt ki u ´j nyelvi eszk¨oz¨ okkel (´ uj f¨ uggv´enyjelek, predik´atumjelek), ´es ezekre nemlogikai axi´om´akat adhat meg – azaz teljesen reprezent´al egy-egy matematikai form´alis elm´eletet. A b˝ov´ıtend˝o logikai rendszer legt¨obbsz¨or persze a term´eszetes levezet´es (NEC.DED). upontban, P´eld´aul a NEC EQU.DED file-t v´alasztva a LOGIC men¨ b´ armely feladat bevitele eset´en az egyenl˝os´eg szab´alyai mindig meg fognak jelenni a v´alaszthat´o levezet´esi szab´alyok k¨oz¨ott. A PEANO.DED az aritmetika Peano-axi´om´ ait foglalja mag´aba (ez a NEC EQU b˝ov´ıt´ese), mely a NEC EQU szab´alyait tov´abb b˝ov´ıti a Peano-axi´om´ak szab´aly-megfogalmaz´as´aval. A GROUP.DED a matematikai csoportelm´elet axi´ om´ aival eg´esz´ıti ki a NEC EQU.DED-et, melyeket minden feladat bevitelekor a felt´etelek el´e f˝ uz. Itt p´eld´aul egy u ´j konstans is bevezet´esre ker¨ ult: o – ez az egys´egelemet jel¨oli. V´eg¨ ul egy nem matematikai t´argyk¨or is megjelenik: a RELATIVE. DED az emberek k¨ozti rokoni kapcsolatokra ad nyelvet ´es axi´om´akat – ennek csak p´elda´ert´eke van. A f¨ uggel´ekben, illetve a [5] munk´aban meg vannak adva a programmal egy¨ utt adott logikai rendszerek – nyelv¨ uk ´es szab´alyaik. ´ Erdemes nekil´atni pl. egy p´ar csoportelm´eleti (csak akkor, ha ismer˝ osek vagyunk arrafele) vagy sz´amelm´eleti t´etel bizony´ıt´as´anak; hamar r´ aj¨ ov¨ unk, milyen neh´ez axiomatikusan fel´ep´ıteni egy matematikai elm´eletet.
20
Deductio
´ LOGIKAI RENDSZER KESZ ´ ´ ´ SAJAT ITESE L´etre kell hoznunk valamilyen ASCII-sz¨ovegszerkeszt˝ovel egy nyelv- ´es levezet´esle´ır´o file-t, helyezz¨ uk el a rendszer hasonl´o file-ai k¨oz´e, ´es a LOGIC men¨ upontban v´alasszuk ezt. Ezt legk¨onnyebb megtenni egy m´ar l´etez˝ o, pl. a NEC.DED p´eld´aj´an. De vigy´azat, biztons´agi m´asolat mindig legyen! Milyen karakterek szerepelhetnek a DEDUCTIO-ban? 512 darab, melyek k¨oz¨ ul az els˝o 256 standard ASCII-karakter, a t¨obbi pedig a program altal gener´alt speci´alis karakter – pl. a logikai jelek. (Ez´ert van sz¨ ´ uks´eg a minimum EGA monitor haszn´alat´ara – t¨obbfajta karakterk´eszlet csak ezeken van. Kisebb kateg´ori´aj´ u grafik´aval is m˝ uk¨odhet a program, csak a speci´alis karakterek hely´en az ASCII-karakterek szerepelnek majd, ´es ez szinte olvashatatlan ´ıgy.) A *.DED file-okban t¨obb szekci´ora van bontva a nyelv- ´es szab´ alyle´ır´ as. A Title (c´ım) szekci´o pontjai: ,,Name” (n´ev), ,,SaveId” (ment´esi azonos´ıt´ o), ,,Description” (le´ır´as). A ,,Name” tartalma jelenik meg a szab´alymen¨ u fels˝ o sor´ aban, a ,,SaveId” tartalm´anak egybe kell esnie a t´enyleges file-n´evvel, a le´ır´as pedig a logika-v´alaszt´o men¨ uben ´ırja le az adott rendszert, a v´ alaszt´ ashoz ad seg´ıts´eget. Ezut´an 3 sor kimarad, ´es egy´ebk´ent is, minden egyes bejegyz´es k¨ozt kimarad egy sor. A Letter Sort szekci´oban a nyelv szignat´ ur´aj´at kell megadnunk. A $ jelek k¨ozt szerepl˝o jelsorok az AMSTEX elnevez´eseit haszn´alj´ ak a nem ASCII-karakterek jel¨ol´es´ere. Viszont azokban az esetekben, ahol bet˝ u(k) van(nak) megadva, ott maga a bet˝ u mellett annak max. n´egy db. sz´ amjeggyel indexelt v´altozatait is haszn´alhatjuk. A nyelvi objektumok tulajdons´agai a k¨ovetkez˝ok: lehets´eges bal jobb precedencia argumentumsz´ am 0. individu´alis v´altoz´ o – – – 1. tempor´ alis individu´alis v´altoz´o – – – 2. f¨ uggv´enyjel 1–9 0–20 0–20 3. tempor´ alis f¨ uggv´enyjel 1–9 0 0–20 4. lok´alis helyettes´ıt´es – 0 3 5. glob´alis helyettes´ıt´es – 0 0 6. predik´ atumjel 1–9 0–20 0–20 7. logikai ¨osszek¨ot˝ojel 1–9 0–20 0–20
´s Nyomtata
21 8. kvantor 9. absztrakt term 10. absztrakt formula
1–9 0 – – – –
2 – –
A *.DED file-okb´ol ki lehet olvasni, hogy az egyes nyelvi k¨ornyezetekben milyen nyelvi objektumokat haszn´alhatunk. Az argumentumsz´ammal rendelkez˝o, m´ask´eppen nem defini´alt bet˝ uk argumentumsz´am´at a feladatban t¨ ort´en˝o els˝o el˝ofordul´asukkor be´ırt argumentumok sz´ama hat´arozza meg (s ha k´es˝obb m´ ashogy haszn´aln´ank, nem fogja elfogadni! ), de a Name Table szekci´oban r¨ ogz´ıthetj¨ uk is egy-egy jel formai le´ır´as´at. Itt minden sorban egy nyelvi szimb´olum ut´an vessz˝ovel elv´alasztva a k¨ovetkez˝o adatokat kell megadni: melyik csoportba tartozik (a fenti felsorol´as sz´ama, 0-t´ ol kezdve), az ¨osszes argumentum sz´ama, ezek k¨oz¨ ul h´any jobboldali, s v´eg¨ ul a precedencia. Azt´an a szab´alyokat kell megadni a Rules szekci´oban, megadva a szab´ aly sorsz´am´at (,,Number”, melyik helyen jelenjen meg a szab´alyv´ alaszt´ o men¨ uben), a szab´aly le´ır´ as´at (,,Rule”, az AMSTEX makr´oneveit haszn´ alva, pl. a ,,\ vdash F1 \ lor F2 \ Rightarrow \ lnot F1 \ & \ lnot F2 \ vdash \ bot” le´ır´ as a ` F 1 ∨ F 2 ⇒ ¬F 1&¬F 2 ` ⊥ szab´alyt ´ırja le. A nev´et is meg kell adni (,,Name”), ez a szab´alyv´ alaszt´ o men¨ uben fog megjelenni, valamint azt a nevet, ami a levezet´es ´abr´ azol´ asaiban megjelenik (,,Anal”), p´eld´ankban: \ lor ai, illetve \ lor i 3, azaz ∨ ai ´es ∨ i 3. Az utols´o szab´alyn´al a ,,Lastrule = Yes” sort is be kell venni. Sz¨ uks´eg eset´en a ,,Strongvar, Nonfreevar” adatokat is be lehet vinni. Ez kvantoros szab´alyokn´al j¨ohet sz´oba – az els˝o esetben a szab´aly alkalmaz´ asa csak akkor megengedett, ha az ¨osszes formul´aban, amely a feladatban szerepel, a megadott v´altoz´o nem szabad, m´ıg a m´asodik esetben megadjuk azt is, mely formul´aban ne szerepelhessen a megadott v´altoz´o. V´eg¨ ul az Axioms szekci´oban az esetleges axi´om´akat kell megadni.
´ NYOMTATAS A konstru´alt levezet´est ki is lehet nyomtatni, miut´an az OPTIONS/ PRINTER DRIVER men¨ upontb´ol kiv´ alasztjuk a megfelel˝o interf´eszprogramot: sajnos egyel˝ore csak az EPS9PRN.EXE ´all rendelkez´esre
22
Deductio
(9 t˝ us Epson), de szerencs´ere ezt nagyon sok nyomtat´o ´erti. Az UTILITIES/PRINT parancs nyomtat. M´asik megold´as az UTILITIES/EXPORT parancscsal AMSTEX form´ aban file-ba menteni, ´es ezzel a programmal b´armely nyomtat´on nyomtathatunk. Ha nem AMS-f´ele TEX-¨ unk van, akkor magunk is defini´ alhatjuk a hi´ anyz´o makr´okat, illetve a k¨ovetkez˝ok a plain TEX-ben is megvannak: \& \supset \lnot \exists \land \rightarrow \Gamma \diamond \bot \Leftrightarrow \epsilon \cap \subset
& ⊃ ¬ ∃ ∧ → Γ ⊥ ⇔ ∩ ⊂
\lor \equiv \forall \sim \dot\lor \leftrightarrow \Delta \top \Rightarrow \vdash \lambda \cup \in
∨ ≡ ∀ ∼ ∨˙ ↔ ∆ > ⇒ ` λ ∪ ∈
´ OS ´ FILE A KONFIGURACI Ez az install´al´asn´al keletkezik DEDUCTIO.CFG n´even. A program m˝ uk¨od´es´ehez sz¨ uks´eges k¨onyvt´ar- ´es file-nevek, valamint a be´all´ıt´ asok alap´ertelmez´ese van benne t´ arolva. K´ezzel is lehet m´odos´ıtani, de vigy´ azni kell, hogy pl. azok a k¨onyvt´arak t´enyleg l´etezzenek, amiket megadunk, valamint a be´all´ıt´asokat helyesen g´epelj¨ uk be! A programban t¨ort´ent be´ all´ıt´ asokat a programban is t´arolni lehet az OPTIONS/SAVE CONFIG paranccsal, ekkor a k¨ovetkez˝o ind´ıt´ askor is ilyen be´all´ıt´asokkal fog jelentkezni a program. A folyamatos konfigur´aci´o-ment´est automatikuss´a lehet tenni az OPTIONS/AUTO SAVE CONFIG paranccsal. A programot ind´ıtani egy´ebk´ent u ´gy lehet, hogy a DEDUCTIO.CFG file k¨onyt´ar´aban ki kell adni a deductio.exe parancsot (ha nem ebben a k¨ onyvt´arban van, akkor az el´er´esi u ´tj´aval egy¨ utt). Az ¨osszes t¨obbi file-t m´ ar megtal´alja, a konfigur´aci´os file-b´ol kiolvasva a hely´et. Ennek seg´ıts´eg´evel pl. NOVELL-h´ al´ ozatban el´eg csak a kiszolg´ al´ o g´ep nyilv´anos merevlemez´ere tenni a programfile-okat, ´es a lok´alis lemezekre
´ cio ´ s file A konfigura
23
csak az egyedi konfigur´aci´os file-t feltenni. P´eld´aul, ha a kiszolg´ al´ o merevlemez´en az F:\DEDUCTIO k¨onyvt´arban tal´alhat´o a program, akkor az oda install´alt konfigur´ac´os fiel-t csak k´et helyen kell v´altoztatni (felt´eve, hogy mi a C:\MY DED k¨onyvt´arban dolgozunk, protokolljainkat a PROT, illetve TEX-export file-ainkat az EXP alk¨onyvt´arakban szeretn´enk tartani): Protocol = C:\MY DED\PROT\uj.prt Print File = D:\MY DED\EXP\uj.tex Ezt a v´altoztatott konfigur´aci´os file-t a lok´alis g´epen helyezz¨ uk el a \MY DED-ben, ´es ott adjuk ki az F:\DEDUCTIO\deductio.exe parancsot, ´es nekikezdhet¨ unk dolgozni.
´ programok Bizony´ıto
24
´ II. RESZ BEVEZET A k¨onyv h´atralev˝o r´esz´eben h´arom bizony´ıt´o programot fogunk bemutatni. A programok bemenete logikai formula, amelyet az adott program megvizsg´al ´es propozicion´alis esetben el is d¨onti, hogy az logikai t¨ orv´eny vagy sem. Az els˝o program neve DTP2 (Debrecen Theorem Prover, version 2). A program Pascal-ban ´ır´odott ´es Turbo Pascal ford´ıt´oval ford´ıtottuk le. A k¨ovetkez˝o program neve LT, ami arra utal, hogy propozicion´ alis logikai formul´ak logikai t¨orv´eny volt´anak ellen˝orz´es´ere lehet igen eredm´enyesen haszn´alni. Ez az´ert van ´ıgy, mert az algoritmusa mindenk´eppen megpr´ob´alja bebizony´ıtani, hogy a formula logikai t¨orv´eny. Ha a formula t´enyleg logikai t¨orv´eny, akkor ez viszonylag gyorsan megy, viszont ha nem logikai t¨orv´eny, az algoritmus minden esetet v´egigpr´ob´al. A program C-ben ´ır´ odott ´es Turbo C-vel lett leford´ıtva. Az utols´o program az LF nevet kapta, mert a formula nem logikai t¨ orv´eny volt´at ellen˝orzi igen gyorsan. Ak´arcsak az el˝obbi, ez is C-ben ´ır´ odott, ´es ugyancsak a Turbo C ford´ıt´oval ford´ıtottuk le. A programok haszn´alat´ahoz a DOS minim´alis ismerete, ´es vagy matematikai logika bevezet˝o kurzus vagy [1] [2] jegyzetek egyik´enek elsaj´at´ıt´asa sz¨ uks´eges. A programok m˝ uk¨od´es´enek meg´ert´es´ehez aj´ anlott [8] is.
´ JELLES A sz´am´ıt´og´epek karakterk´eszleteiben hi´aba is keress¨ uk a logik´ aban megszokott jeleket. Ez´ert k´enytelenek vagyunk m´as karaktereket haszn´ alni. Ezek a karakterek u ´gy lettek kiv´alasztva, hogy valamelyest utaljanak arra a jelre, melyet helyettes´ıtenek. ≡ ⊃ ∧ ∨ ¬ ∀ ∃
= > & | − ˆA ˆE
¨ le ´s Jelo
25
L´assunk egy p´eld´at: a (∃x(A(x) ⊃ B(x)) ≡ (∃y¬A(y) ∨ ∃zB(z))) formul´at a k¨ovetkez˝ok´eppen ´ırhatjuk: (ˆEx(A(x) > B(x)) = (ˆEy − A(y))|(ˆEzB(z))) Ha ilyen vagy hosszabb formul´at g´epel¨ unk be, akkor k¨onnyen elfelejthet¨ unk bez´arni egy-k´et z´ar´ojelet. El´eg k´enyelmetlen m´ar csak beg´epelni is az ¨ osszes z´ar´ ojelet, nem hogy m´eg ellen˝or´ızni is. Szerencs´ere van lehet˝ os´eg cs¨ okkenteni a z´ar´ojelek sz´am´at. Ha a formul´ankban az utols´o logikai ¨ osszek¨ ot˝ojel a ∧, ∨, ⊃, ≡ jelek egyike, akkor a legk¨ uls˝o z´ar´ojelet elhagyhatjuk. 2 (x2 ) Matematik´aban a ( 2 ) − 1 helyett csak x2 − 1-t ´ırunk, mert tudjuk hogy a hatv´anyoz´as er˝osebben k¨ot mint az oszt´as, ´es az oszt´as er˝ osebben k¨ ot mint a kivon´as. A logikai jelek k¨oz¨ott is van ilyen sorrend. A k¨ ovetkez˝ o t´ abl´azatban a fentebb tal´alhat´o jelek er˝osebbek mint a lentebb lev˝ ok. ∃ ∀ ¬ ∧ ∨ ⊃ ≡ Ezek szerint a (((A ∧ B) ⊃ (B ∨ A)) ≡ (¬A ⊃ B)) formula helyett elegend˝ oa A ∧ B ⊃ B ∨ A ≡ ¬A ⊃ B formul´at ´ırnunk. Az aritmetikai kifejez´esekn´el melyek t¨obb azonos er˝oss´eg˝ u jelet tartalmaznak balr´ ol jobbra haladva kapjuk meg a v´egeredm´enyt, ´ıgy p´eld´ aul a 12/6 ∗ 4 eredm´eny¨ ul 8-at ad. Ilyen egy´ertelm˝ u szab´aly a logik´aban nem terjedt el, ez´ert azonos er˝oss´eg˝ u, ´am k¨ ul¨onb¨ oz˝o logikai ¨osszek¨ot˝o jelek eset´en mindig haszn´aljunk z´ar´ojelez´est. Megvizsg´alhatjuk (p´eld´aul az itt le´ırt programokkal) hogy a A ∧ (B ∨ C) nem ugyanaz mint az (A ∧ B) ∨ C.
´ programok Bizony´ıto
26
A z´ ar´ojelet egyforma er˝oss´eg˝ u jelek k¨oz¨ott csak akkor hagyhatjuk el, ha ezek a jelek mind ∧ vagy mind ∨ jelek (teh´at az (A ∧ (B ∧ C)) helyett ´ırhatunk A ∧ B ∧ C-t is). Viszont vigy´azzunk az implik´aci´ora! (Vizsg´ aljuk meg az (A ⊃ (B ⊃ C) ≡ ((A ⊃ B) ⊃ C) formul´at! L´athatjuk, itt igencsak fontos a z´ar´ojel!) M´ar ezzel is igen sok z´ar´ojelt˝ol szabadultunk meg, de m´eg tov´ abbiakt´ ol is megszabadulhatunk. Ezt a pontok haszn´alata teszi lehet˝ov´e, ahol egy z´ ar´ojelen bel¨ ul a leggyeng´ebb jelet az ut´ana tett ponttal jel¨olj¨ uk meg, ´ıgy p´eld´aul az ((A ⊃ B) ∧ (B ⊃ A)) formula helyett ezent´ ul el´eg A ⊃ B ∧ . B ⊃ A-t ´ırnunk. Mivel a pontok haszn´alata igen k´enyelmes, bevezett´ek a kett˝ospontot is, amely azt a logikai ¨osszek¨ot˝ojelet jel¨oli, mely gyeng´ebb (´es ez´ert k´es˝obben hat) az ¨osszes ponttal jel¨olt logikai ¨osszek¨ot˝ojeln´el. Ezek szerint a ¬ : A ≡ B ⊃ .A ∨ ¬B formula a ¬((A ≡ B) ⊃ (A ∨ ¬B)) formul´anak felel meg. Most m´ ar mindent tudunk, ami sz¨ uks´eges lehet a programok haszn´ alat´ ahoz.
DTP 2 L´assuk az els˝o programot. A programot a dtp-2 vagy a dtp-2t beg´epel´es´evel ind´ıtjuk el. Az ut´ obbi esetben a program kicsit b˝obesz´ed˝ ubb, ´am a l´enyeges dolgokat az els˝ o esetben is megtudjuk. Ezut´an megjelenik a kezd˝o k´eperny˝o: D T P - 2 Theorem Prover Do you want to print?
y/n-
Itt megadhatjuk, hogy a program nyomtat´ora kinyomtassa-e az eredm´enyt. Az egyszer˝ u felhaszn´al´o, aki csak a v´egeredm´enyre k´ıv´ancsi, azaz arra, hogy az adott formula logikai t¨orv´eny vagy sem ´es nem akarja a k´es˝ obbiekben elemezni a feladat megold´as´at, az itt az n-et v´alasztja. Mi is ezt tesz¨ uk most. Ezut´an a Do you work from disk?
y/n-
k´erd´esre adott n v´alasz ut´an be kell g´epeln¨ unk azt a formul´ at, melyre k´ıv´ ancsiak vagyunk.
DTP 2
27 Please, write your formula:
A predik´atumaink, f¨ uggv´enyv´altoz´oink nev´enek az angol ´ab´ec´e egyik bet˝ uj´evel kell kezd˝odnie ´es ezt maximum k´et sz´amjegy k¨ovetheti. Most pr´ obak´epp egy nem logikai t¨orv´eny formul´at adunk meg. (A|B>C)=(A>C)|(B>C)@ Ha a formula nem f´er el egy sorba, akkor azt t¨obb sorba is ´ırhatjuk. A jobb olvashat´os´ag kedv´e´ert sz´ok¨oz¨oket vagy ak´ar u ¨res sorokat is besz´ urha´ tunk a formul´aba. Epp ez´ert a formula v´eg´et egy @ karakterrel kell jel¨ oln¨ unk. Ez a karaktersorozat az (A ∨ B ⊃ C) ≡ (A ⊃ C) ∨ (B ⊃ C) formul´anak felel meg. N´ezz¨ uk mit ad erre a program, ´es ezeknek mi a jelent´ese: Original formula: (A|B>C)=(A>C)|(B>C)@ A program m´eg egyszer ki´ırja a formul´ankat abban az alakban, ahogy mi beg´epelt¨ uk. Ez akkor igaz´an hasznos, ha lemezr˝ol olvassuk be a formul´ at vagy ha kinyomtatjuk a megold´ast. Full formula: (((A[0]|B[0])>C[0])=((A[0]>C[0])|(B[0]>C[0])))@ A program a formula teljes z´ar´ojelezett alakj´at ´ırja ki. A most k¨ ovetkez˝o fogalmakat nem t´argyalja a bevezet˝o logika kurzus. Ezen fogalmakkal a mesters´eges intelligencia kurzusban tal´alkozhatunk, de a [8]ban is megtal´alhatjuk. polish form &>>|A[0]B[0]C[0]|>A[0]C[0]>B[0]C[0]>|>A[0]C[0] >B[0]C[0]>|A[0]B[0]C[0]@ Ezek ut´an a – sz´am´ıt´og´ep sz´am´ara fogyaszthat´obb – lengyel ´abr´ azol´ asban (amikor is a logikai ¨osszek¨ot˝ojelek nem a r´eszformul´ak k¨oz¨ott, hanem el˝ ott¨ uk szerepelnek) l´atjuk u ´jra formul´ankat. skolem form &>>|A[0]B[0]C[0]|>A[0]C[0]>B[0]C[0]>|>A[0]C[0] >B[0]C[0]>|A[0]B[0]C[0]@
28
´ programok Bizony´ıto
Most semmi nem v´altozott, ´am ha az eredeti formula tartalmazott volna kvantorokat, akkor azokt´ol a Skolem forma alkalmaz´as´aval megszabadulhatunk (esetleg u ´gy, hogy u ´j f¨ uggv´enyjeleket vezet¨ unk be). normal form &-&-&-&-A[0]-B[0]-C[0]&&A[0]-C[0]&B[0]-C[0]-&-&&A[0] -C[0]&B[0]-C[0]&-&-A[0]-B[0]-C[0]@ A el˝oz˝o formul´at konjunkt´ıv norm´al form´aba ´ırja a program. Basic replica: B[0]?A[0],C[0];A[0]?B[0],C[0]@ List of metavariables of the basic replica: @ A formul´ankat szekvent jel¨ol´esben tartalmazza a Basic replica, ´ıgy az el˝ obbi karaktersorozat a (B → A, C); (A → B, C)-t jelenti. Ha a formula nem tartalmaz kvantorokat, akkor azt m´ar egyszer˝ uen megkapjuk, hogy a formula logikai t¨orv´eny-e vagy sem, viszont ha tartalmaz kvantort, akkor a program elindul a formula elej´et˝ol ´es megfelel˝o u ´j v´altoz´okat keres. Ha nagyon sok´aig nem jut eredm´enyre, akkor ugyanezt megpr´ob´alja a formula v´eg´er˝ol elindulva is. Mivel a p´eld´ankban szerepl˝o formula nem tartalmaz kvantorokat, ´ıgy azonnal megkapjuk a v´alaszt. The original formula is undeducible Is there any other formula yet? y/nA sz´amunkra legfontosabb inform´aci´o az utols´o el˝otti sorban tal´ alhat´ o, az undeducible sz´o azt jelenti, hogy ez a formula nem levezethet˝ o. Pr´ob´aljuk ki, mik´epp v´alaszol a program egy logikai t¨orv´enyre, ´epp ez´ert az utols´o sorban tal´alhat´o k´erd´esre (azaz arra, hogy m´eg akarjuk-e haszn´alni a programot) v´alaszoljunk y-nal. Please, write your formula: (A&B>C)=(A>C)|(B>C)@ Original formula: (A&B>C)=(A>C)|(B>C)@ Full formula: (((A[0]&B[0])>C[0])=((A[0]>C[0])|(B[0]>C[0])))@ Basic replica: @ List of metavariables of the basic replica:
DTP 2
29
@ The original formula is deducible Is there any other formula yet? y/nMint l´atjuk itt m´ar m´ast ´ırt ki a program, a deducible azt jelenti hogy a formul´ank levezethet˝o. (Ezen nem is csod´alkozhatunk, hisz a formul´ ank logikai t¨orv´eny.) N´ezz¨ uk meg mi t¨ort´enik, ha elt´evesztj¨ uk az egyik formul´at: Please, write your formula: (A|B)>(A&B))@ Original formula: (A|B)>(A&B))@ There is an error in the formula! Is there any other formula yet? y/nL´atjuk nem t¨ort´ent semmi baj, de a formul´ankat – k´enytelen-kelletlen – u ´jra be kell g´epelni. Ez hosszabb formula eset´en igen k´enyelmetlen. Ez´ert sokkal jobban j´arunk, ha egy sz¨ovegszerkeszt˝ovel egy file-ba ´ırjuk a formul´ankat, amit ´ıgy (esetleg a program hibajelz´ese ut´an) ut´ olag is ki tudunk jav´ıtani. A lemezmell´ekleten a DTP2 alk¨onyvt´arban t¨obb el˝ore beg´epelt p´eld´ at tal´ alunk. P´eld´aul a (P ≡ Q) ≡ ((Q ∨ ¬P ) ∧ (¬Q ∨ P )) formul´at a c14.f file tartalmazza. formul´at: A
N´ezz¨ uk hogyan tesztelhetj¨ uk ezt a
Do you work from disk?
y/n-
k´erd´esre y-t v´alaszoljunk. Ezut´an a Name of file? k´erd´esre most a c14.f a helyes v´alasz. Ezek ut´an a k¨ovetkez˝ok jelennek meg a k´eperny˝on: Original formula: P=Q=:Q|-P&.-Q|P@ Full formula: ((P[0]=Q[0])=((Q[0]|-P[0])&(-Q[0]|P[0])))@ Basic replica:
30
´ programok Bizony´ıto
@ List of metavariables of the basic replica: @ The original formula is deducible Is there any other formula yet? y/nM´ar tudjuk, ez azt jelenti, hogy a formul´ank logikai t¨orv´eny. Pr´ ob´ aljunk ki m´eg egy-k´et formul´at! (Azaz nyomjunk y-t. Ha m´egis m´ ask´epp d¨ ont¨ unk, a programb´ol kil´ephet¨ unk n lenyom´as´aval.) Ismert, hogy a kvantort nem tartalmaz´o (´ıt´eletkalkulusi) formul´ akr´ ol algoritmussal eld¨onthetj¨ uk logikai t¨orv´eny-e vagy sem. Olyan algoritmus viszont, amely ugyanezt minden formul´ar´ol eld¨ontse nincs. A DTP2 megpr´ ob´ alkozik a sz´am´ara feladott kvantoros formul´akkal, ´am el˝ofordulhat hogy nem tudja eld¨onteni a k´erd´est, ´ıgy p´eld´aul a ∃y∀x(A(x, y) ≡ A(x, x)) ⊃ ¬∀x∃y∀z(A(x, y) ≡ ¬A(z, x)) formula eset´en sem: Original formula: ^Ey^Ax(A(x,y)=A(x,x))> -^Ax^Ey^Az(A(x,y)=-A(z,x))@ Full formula: (^Ey^Ax(A[2](x,y)=A[2](x,x))> -^Ax^Ey^Az(A[2](x,y)=-A[2](z,x)))@ Basic replica: A[2]zu1?A[2]xa0,A[2]xx,A[2]u1f[1]0u1; A[2]u1f[1]0u1?A[2]xa0,A[2]xx,A[2]zu1 ;A[2]xx,A[2]xa0,A[2]zu1?A[2]u1f[1]0u1; A[2]xx,A[2]xa0,A[2]u1f[1]0u1?A[2]zu1@ List of metavariables of the basic replica: xu1z@ Kis id˝o m´ ulva megkapjuk a v´egeredm´enyt. I can’t decide it Is there any other formula yet? y/nTerm´eszetesen vannak olyan kvantoros formul´ak, melyeket a program el tud d¨onteni: Please, write your formula:
DTP 2
31
^Ex^AyP(x,y)>^Ay^ExP(x,y)@ Original formula: ^Ex^AyP(x,y)>^Ay^ExP(x,y)@ Full formula: (^Ex^AyP[2](x,y)>^Ay^ExP[2](x,y))@ Basic replica: P[2]a1y?P[2]u0a0@ List of metavariables of the basic replica: yu0@ The cycle number is 1 The mode is 1 The original formula is deducible V´eg¨ ul l´assunk egy olyan kvantoros formul´at, mely nem logikai t¨ orv´eny: Original formula: ^Ax.A(x)|B(x)>:^ExA(x)@ Full formula: (^Ax(A[1](x)|B[1](x))>^ExA[1](x))@ polish form >^ Ax|A[1]xB[1]x^ExA[1]x@ skolem form >|A[1]xB[1]xA[1]u0@ normal form -&-&-A[1]x-B[1]x-A[1]u0@ Basic replica: A[1]x?A[1]u0;B[1]x?A[1]u0@ List of metavariables of the basic replica: xu0@ The cycle number is 1 The mode is 1 The original formula is undeducible
´ programok Bizony´ıto
32
´ LT LF ES Ezt a k´et programot egyszerre t´argyaljuk, mert ugyanazzal a felhaszn´ al´oi fel¨ ulettel rendelkeznek. Pontosabban nem rendelkeznek semmilyen fel¨ ulettel, ´am ´erz´esem szerint ´ıgy sokkal jobban haszn´alhat´oak a programok. A programot a k¨ovetkez˝ ok´eppen ind´ıthatjuk: LF [file-n´ev] [darabsz´ am] A sz¨ogletes z´ar´ojelek azt jelentik, hogy az abban szerepl˝o tag ak´ ar el is ´ hagyhat´o. Igy p´eld´aul helyes programind´ıt´asok a k¨ovetkez˝ok: LF LF pelda LF pelda 100 Az els˝o esetben a program a sor.xpl nev˝ u file-ban tal´alhat´o formul´ akat teszteli. M´asodik esetben a pelda file-ban tal´alhat´o formul´akkal foglalkozik. Harmadik esetben ugyancsak a pelda formul´ait vizsg´alja meg, ´ am ekkor nem egyszer, hanem pontosan sz´azszor; ez teszi lehet˝ov´e sz´ amunkra, hogy a programokat sebess´eg¨ uk alapj´an ¨osszehasonl´ıthassuk. Ha t¨ obbsz¨ or futtatjuk a programot ugyanazon formul´ara (utols´o eset), a program annyiszor ´ırja ki a formul´ankr´ol, hogy az logikai t¨orv´eny-e vagy sem, ah´ anyszor ezt megvizsg´alja. Ha ez zavar benn¨ unket, akkor a kimenetet egy file-ba vezethetj¨ uk, ´ıgy p´eld´aul: LF pelda 100 > kimenet.out Mint l´atjuk itt a formul´ankat mindenk´eppen egy file-ba kell ´ırnunk. ´ Legk¨onnyebben ezt egy sz¨ovegszerkeszt˝ovel tehetj¨ uk meg. (Erdemes programsz¨oveg-szerkeszt˝ot haszn´alni, mert a bemenet csak ASCII karaktereket tartalmazhat, ez´ert ha valaki a kedvenc sz¨ovegszerkeszt˝oj´et szeretn´e haszn´ alni, az a formul´akat ASCII form´atumban mentse ki.) Ha valamilyen okb´ ol nincs a k¨ozelben sz¨ovegszerkeszt˝o, haszn´alhatjuk a k¨ovetkez˝o tr¨ ukk¨ ot: copy con: pelda[Enter] --P>P[Enter] [Enter] [F6] [Enter] (Itt az [Enter] jel¨oli az Enter felirat´ u billenty˝ u le¨ ut´es´et.) Ezzel a m˝ uvelettel a pelda file-ba be´ırtuk a ¬¬P ⊃ P formul´ at. Megfigyelhetj¨ uk, hogy egy u ¨res sort kell a formula ut´an be´ırni. Ez az´ert van ´ıgy, mert egy file t¨obb formul´at is tartalmazhat, ´es a formul´akat egy u ¨res sorral v´alasztjuk el. A program term´eszetesen a file-ban tal´alhat´ o ¨ osszes
´s LT LF e
33
formul´at feldolgozza. Az utols´o formul´at lez´ar´o [Enter] ut´an is kell m´eg egy [Enter] -t u ¨tn¨ unk, mert k¨ ul¨onben nem dolgozza fel az utols´o formul´ at. Hogy min´el egyszer˝ ubb legyen a program, a predik´atumainkat csak egy bet˝ uvel jel¨olhetj¨ uk. Nem vagyunk csak 26 predik´atumra korl´ atozva (az angol ´ab´ec´e bet˝ uire), mert a kis- ´es a nagybet˝ uk m´ast jelentenek. (Ez´ert a A ≡ a ´epp´ ugy nem logikai t¨orv´eny mint az A ≡ B.) Ez a k´et program csak ´ıt´eletkalkulusi formul´akra alkalmazhat´ o, kvantoros formul´akat el sem fogadnak a programok. Tov´abbi b´ ar nem l´enyeges megszor´ıt´as az, hogy ez a k´et program nem ismeri az ekvivalencia m˝ uveletet, ´ıgy azt teljes form´aban (azaz A = B helyett A > B&.B > A-t) kell le´ırni. A program vagy igen sz˝ ukszav´ u, vagy nagyon b˝obesz´ed˝ u (A b˝ obesz´ed˝ ubb verzi´okat az LFL vagy LTL n´evvel ind´ıthatjuk, ahol az L bet˝ u a long sz´ ora utal. Vizsg´aljunk meg p´ar formul´at az LF programmal: lf p.1 (C>-A|B)&-(-(C>A)|.C>B)>-(C|-(A&R)) The original formula is deducible Used memory : 18 Done Azaz ez a formula logikai t¨orv´eny, m´ıg a k¨ovetkez˝o nem lesz az. lf p.2 (A|B>C)>(A>C&B>.C)&.(A>C&B>.C)>(A|B>C) The original formula is undeducible Used memory : 25 Done A Done sz´ocska azt jelzi, hogy az adott file-ban az ¨osszes formul´ at feldolgozta a program. Mi t¨ort´enik ha egy formul´at hib´asan adunk meg? lf p.3 (P&(Q>R)>A>.(-P|Q|A&.-P|-R|A) Error! Too many ( I can’t continue! Done
´ programok Bizony´ıto
34
L´assuk hogy m˝ uk¨odik a program! Ehhez az LFL programot kell elind´ıtani, viszont az ¨osszes inform´aci´o nem f´er el a k´eperny˝ore. Ez´ert a kimenetet ir´ any´ıtsuk file-ba: lfl p.4 > eredmeny Ezt a file-t vagy egy sz¨ovegszerkeszt˝o programmal n´ezhetj¨ uk meg, vagy pedig a DOS TYPE parancs´at haszn´alhatjuk: type eredmeny. Az ut´ obbi esetben a list´az´ast felf¨ uggeszthetj¨ uk a PAUSE, tov´abbengedhetj¨ uk az ENTER billenty˝ u lenyom´as´aval. Az eredmeny file tartalma a k¨ ovetkez˝ o: (A>B)>A>.A t(A>B)>A>A f(A>B)>A/tA t(A>B)/fA/tA fA/tB/fAtA tB/fA/tA fA/tA tA 0 / +(*(+(fA,tB),fA),tA) 0 / +(*(^,^),v) 0 / +(^,v) 0 /^ The original formula is deducible Used memory : 6 Done Az algoritmus l´ep´esei a k¨ovetkez˝ok: el˝osz¨or a formul´at ´at´ırjuk point– plus alakba, majd a formul´at erre az alakra vonatkoz´o egyszer˝ u logikai t¨ orv´enyek alapj´an megpr´ob´aljuk egyszer˝ us´ıteni, esetleg t¨obb r´eszre bontani (amelyek ∧-sel kapcsol´odnak ¨ossze), ´es olyan ´ert´ekel´est keres¨ unk mellyel valamely r´esz hamis lesz, mert ha ez siker¨ ul az eg´esz formula nem lehet logikai t¨orv´eny. N´ezz¨ uk a m´asik programot, az LT-t. lt p.1 (C>-A|B)&-(-(C>A)|.C>B)>-(C|-(A&R)) The estimated length in sequent notation is 5 cluster and in cosequent notation 18 cluster The original formula is deducible
´s LT LF e
35
Done A kor´abbiakb´ol v´arhat´o volt, hogy ez a formula t´enyleg logikai t¨ orv´eny. Ez a program is ´atalak´ıtja a formul´at pp-alakra, majd e jel¨ol´es dualit´ as´ at kihaszn´alva pr´ob´alja egyszer˝ us´ıteni a formul´at. lt p.2 (A|B>C)>(A>C&B>.C)&.(A>C&B>.C)>(A|B>C) The estimated length in sequent notation is 20 cluster and in cosequent notation 10 cluster The original formula is undeducible Done Hib´as formula eset´en ugyan´ ugy viselkedik az LT, mint az LF: lt p.3 (P&(Q>R)>A>.(-P|Q|A&.-P|-R|A) Error! Too many ( I can’t continue! Done L´assuk hogyan is dolgozik a program: ltl p.4 > eredmeny Az eredmeny file els˝o r´esz´et felesleges ide m´asolni, mert ugyanaz mint el˝ obb. A m´asodik r´esz: The estimated length in sequent notation is 3 cluster and in cosequent notation 2 cluster fA tA/fA fB/tA/fA tA/fB/tA/fA tAfB/tA/fA tA/fA v The original formula is deducible Done
36
´ IRODALOMJEGYZEK [1] Drag´alin–B´ uz´asi: Bevezet´es a matematikai logik´aba. KLTE egyetemi jegyzet, 1986 [2] P´asztorn´e Varga Katalin: Matematikai logika ´es alkalmaz´asai. Budapest, ELTE egyetemi jegyzet, 1989 [3] Bell–Machover: A course in mathematical logic. Amsterdam–New York– Oxford, North-Holland, 1977 [4] Hilbert–Bernays: Grundlagen der Mathematik, m´asodik kiad´ as, Berlin– Heidelberg–New York, Spinger, 1970 [5] Smirnov–Novodvorsky: Language for logical systems description. ILCSDP, Moscow, 1993 [6] DEDUCTIO User Guide. ILCSDP, Moscow, 1993 [7] DEDUCTIO Reference Manual. ILCSDP, Moscow, 1993 [8] Drag´alin–Aszal´os–Horv´ath: A practical-oriented deducibility algorithm for propositional logic: duality and limited resolution, BAM 784/92 (LXI), 1992, pp. 102-114.
