Esmakordselt avaldatud teisipäeval 13. juunil 2006; sisuline läbivaatamine reedel 24. märtsil 2017
Hübriidloogika on loogika, mille tulemuseks on tavalisele modaalloogikale täiendava väljendusjõu lisamine. Kõige elementaarsem hübriidloogika saadakse niinimetatud nominaalide lisamisega, mis on uut laadi algsümbolid, mis kõik vastavad tõele täpselt ühes võimalikus maailmas. Hübriidloogika ajalugu ulatub tagasi Arthur N. Priori loomingusse 1960ndatel.
1. Hübriidloogika motivatsioonid
2. Formaalne semantika
3. Tõlked
4. Arthur N. Eelnev ja hübriidloogika
5. Hübriidloogika arendamine alates eelmisest
6. Hübriidloogika aksioomid
7. Hübriidloogika analüütilised tõestusmeetodid
Bibliograafia
Akadeemilised tööriistad
Muud Interneti-ressursid
Seotud kirjed
1. Hübriidloogika motivatsioonid
Kripke'i modaalloogika standardses semantikas on tõde komplekti punktide suhtes. Seega võib algsümbolil olla erinevate punktide suhtes erinevad tõeväärtused. Tavaliselt võetakse neid punkte arvesse võimalike maailmade, aegade, episteemiliste olekute, arvuti olekute või millegi muu jaoks. See võimaldab meil vormistada loomuliku keele väited, mille tõeväärtused on näiteks ajaga võrreldes sarnased
sajab
millel on eri aegadel selgelt erinevad tõeväärtused. Nüüd kehtivad teatud looduskeele väited täpselt ühe korraga, võimaliku maailma või millegi muuga. Näitena võib tuua väite
Kell on 15. märts 2006 kell viis
mis on tõsi ajal kell viis 15. märts 2006, kuid on vale muul ajal. Esimest tüüpi looduskeele avaldusi saab vormistada tavalises modaalses loogikas, kuid teist tüüpi mitte.
Hübriidloogika peamine motivatsioon on tavalisele modaalloogikale täiendava väljendusjõu lisamine eesmärgiga suuta vormistada teist laadi väited. See saadakse tavalise modaalloogika lisamisega teist tüüpi algsümboliteks, mida nimetatakse nominaalideks, nii et Kripke semantikas on iga nominaal tõene ühe punkti suhtes. Seejärel vormistatakse teist laadi loomuliku keele avaldus (nagu näitelause kellaajaga kell 15, 15. märts 2006), kasutades nominaalset, mitte tavalist ettepanekusümbolit (mida kasutataks vihmase ilmaga näitelause vormistamiseks). Fakt, et nominaalne on täpselt ühe punkti suhtes tõene, tähendab, et nominaali võib pidada punktile viitavaks terminiks, näiteks kui (mathtt {a}) on nominaal, mis tähistab “see on viis o kell 15 märts 2006,siis võib seda nominaali pidada terminiks, mis viitab kellaajale kella 15-ni 15. märtsil 2006. Seega on hübriidloogikas spetsiifiline ettepanekusümbol, samas kui esimese järgu loogikas on see argument predikaadiks.
Enamik hübriidloogikaid hõlmab täiendavaid lisaseadmeid kui nominaalid. Täiendavate masinate lisamiseks on mitmeid võimalusi; siin kaalume nn rahulolu operaatoreid. Rahuloluoperaatorite lisamise motivatsiooniks on võimalus vormistada väide, mis vastab tõele konkreetsel ajal, võimalikul maailmas või milleski muus. Näiteks tahame, et saaksime vormistada, et väide „sajab vihma” on tõsi ajal kell viis 15. märts 2006, see tähendab, et
kell viis 15. märtsil 2006 sajab vihma.
See vormistatakse valemiga (mathtt {@_ a p}), kus nominaalne (mathtt {a}) tähendab ülaltoodud tähendust: „kell on 15. märts 2006 kell viis ja kus (mathtt {p}) on tavaline algsümbol, mis tähistab sõna "sajab vihma". Seda valemi (mathtt {@_ a p}) osa (mathtt {@_ a}) nimetatakse rahuloluoperaatoriks. Üldiselt, kui (mathtt {a}) on nominaalne ja (mathtt { phi}) on suvaline valem, siis uus valem (mathtt {@_ a \ phi}) nimetatakse a saab üles ehitada rahulolu avalduse. Rahulolu avaldus (mathtt {@_ a \ phi}) väljendab, et valem (mathtt { phi}) vastab ühe konkreetse punkti suhtes, nimelt sellele, kus nominaalne (mathtt {a }) viitab.
Kokkuvõtteks võib öelda, et oleme nüüd tavalisele modaalloogikale nominaalide ja rahulolu operaatorite näol täiendanud väljendusjõudu. Mitteametlikult on nominaalsel (mathtt {a}) tõesus
(mathtt {a}) on punkti (w) suhtes tõene
siis ja ainult siis, kui viide (mathtt {a}) on identne (w)
ja rahulolukinnitusel (mathtt {@_ a \ phi}) on tõesus
(mathtt {@_ a \ phi}) vastab punkti (w) suhtes tõele
siis ja ainult siis, kui
(mathtt { phi}) on tõsi, võrreldes viitega (mathtt {a })
Pange tähele, et tegelikult punkt (w) ei oma (mathtt {@_ a \ phi}) tõesuse tingimustes tähtsust, kuna rahulolu operaator (mathtt {@_ a}) liigutab hindamispunkti viitega (mathtt {a}) olenemata (w) identiteedist.
On tähelepanuväärne, et nominaalid koos rahulolu operaatoritega võimaldavad meil väljendada, et kaks punkti on identsed: Kui nominaadid (mathtt {a}) ja (mathtt {b}) viitavad punktidele (w) ja (v), siis väljendab valem (mathtt {@_ a b}), et (w) ja (v) on identsed. Järgmine mõttekäik näitab, miks.
(mathtt {@_ a b}) on punkti (w) suhtes tõene
siis ja ainult siis, kui
(mathtt {b}) vastab tõele (mathtt {a})
siis ja ainult siis, kui
(mathtt {b}) vastab tõele (w), siis ja ainult siis, kui viide (mathtt {b}) on identne (w), siis ja ainult kui
(v) on identne (w)
Identiteedi seosel komplektil on tuntud omadused refleksivus, sümmeetria ja transitiivsus, mis kajastub selles, et valemid
) alusta {joonda *} ja \ mathtt {@_a a} & \ mathtt {@_ a b \ paremääris @_b a} & (mathtt {@_ a b \ amp @_b c) rightarrow @ _a c} lõpeta {joonda *})
Nominaalide ja rahulolukorraldajate kõrval vaatleme alljärgnevas nn sideaineid (mathtt { forall}) ja (mathtt { downarrow}), mis võimaldavad meil valemeid luua (mathtt { forall a \ phi}) ja (mathtt {{ downarrow} a \ phi}). Sideained seovad nominaalid punktidega kahel erineval viisil: (mathtt { forall}) köidab kvantifitseerides punkte, mis on analoogsed standardse esimese järgu universaalse kvantifikaatoriga, see tähendab, (mathtt { forall a \ phi}) on tõsi (w) suhtes juhul ja ainult siis, kui mis iganes punktile nominaalne (mathtt {a}) viitab, on (mathtt { phi}) tõene (w). Sideaine (mathtt { downarrow}) seob nominaali hindamispunktiga, see tähendab, et (mathtt {{ downarrow} a \ phi}) on tõsi (w) suhtes, kui ja ainult siis, kui (mathtt { phi}) vastab tõele (w), kui (mathtt {a}) viitab (w). Selgub, et sideaine (mathtt { downarrow}) on defineeritav järgmiselt: (mathtt { forall}) (nagu allpool näidatud).
2. Formaalne semantika
Keel, mida me peame, on tavalise modaaloogika loogika, mis on üles ehitatud tavalistele algsümbolitele (mathtt {p}, \ mathtt {q}, \ mathtt {r},…), samuti nominaalidele (mathtt {a}, \ mathtt {b}, \ mathtt {c},…) ja laiendatud rahulolu operaatorite ja sideainetega. Me võtame juhendühendused (mathtt { kiil}) ja (mathtt { neg}) primitiivseks; muud ettepanekul põhinevad ühendused on määratletud nagu tavaliselt. Samamoodi võtame modaaloperaatori (mathtt { Box}) primitiivsena ja defineerime modaaloperaatori (mathtt { Diamond}) kui (mathtt { neg \ Box \ neg}). Nagu nimigi ütleb, seovad sideained nominaale ja nominaalide vaba ja seotud esinemise mõisted määratletakse analoogselt esimese järgu loogikaga. Rahuloluoperaatorid ei seo nominaale, stvabad nominaalsed esinemised valemis (mathtt {@_ a \ phi}) on tasuta nominaalsed esinemised kaustas (mathtt { phi}) koos (mathtt {a}) esinemisega. Lasime, et (mathtt { phi [c / a]}) oleks valem (mathtt { phi}), kus nominaalne (mathtt {c}) on asendatud kõigi vabade esinemistega nominaalne (mathtt {a}). Kui nominaalne (mathtt {a}) ilmub vabalt rakenduses (mathtt { phi}) (mathtt { forall c}) või (mathtt {{ downarrow} c}), siis seotakse nominaalne (mathtt {c}) jaotises (mathtt { phi}) ümber vastavalt vajadusele. Kui nominaalne (mathtt {a}) ilmub vabalt rakenduses (mathtt { phi}) (mathtt { forall c}) või (mathtt {{ downarrow} c}), siis seotakse nominaalne (mathtt {c}) jaotises (mathtt { phi}) ümber vastavalt vajadusele. Kui nominaalne (mathtt {a}) ilmub vabalt rakenduses (mathtt { phi}) (mathtt { forall c}) või (mathtt {{ downarrow} c}), siis seotakse nominaalne (mathtt {c}) jaotises (mathtt { phi}) ümber vastavalt vajadusele.
Nüüd määratleme mudelid ja raamid. Hübriidloogika mudeliks on kolmekordne ((W, R, V)), kus (W) on mittetühi komplekt, (R) on (W) binaarsuhe ja (V) on funktsioon, mis igale paarile, mis koosneb elemendist (W) ja tavalisest algsümbolist, määrab hulga elemendi ({0,1 }). Paari ((W, R)) nimetatakse kaadriks. Seega on mudelid ja raamid samad, mis tavalisel modaaloogikal. (W) elemente nimetatakse maailmadeks ja seost (R) nimetatakse juurdepääsetavuse suheteks. Öeldakse, et mudel ((W, R, V)) põhineb raamil ((W, R)).
Mudeli (M = (W, R, V)) omistamine on funktsioon (g), mis igale nominaalile määrab elemendi (W). Ülesanne (g ') on (mathtt {a}) muutuja (g) -variandist, kui (g') nõustub (g) kõigi nominaalidega, kui võimalik salvestada (mathtt {a}). Seos (M, g, w \ vDash \ phi) on defineeritud induktsiooni abil, kus (g) on ülesanne, (w) on (W) element ja (mathtt { phi}) on valem.
(M, g, w \ vDash \ mathtt {p}) iff (V (w, \ mathtt {p}) = 1)
(M, g, w \ vDash \ mathtt {a}) iff (w = g (mathtt {a}))
(M, g, w \ vDash \ mathtt { phi \ wedge \ psi}) iff (M, g, w \ vDash \ mathtt { phi }) ja (M, g, w \ vDash \ mathtt { psi})
(M, g, w \ vDash \ mathtt { neg \ phi}) kui pole (M, g, w \ vDash \ mathtt { phi})
(M, g, w \ vDash \ mathtt { Box} phi) kui iganes elemendi (v) jaoks on (W) nii, et (wRv), on nii, et (M, g, v \ vDash \ mathtt { phi})
(M, g, w \ vDash \ mathtt {@_ a \ phi}) iff (M, g, g (mathtt {a}) vDash \ mathtt { phi})
(M, g, w \ vDash \ mathtt { forall a \ phi}) iff with any (mathtt {a}) - (g) variandist (g '), nii on, et (M, g', w \ vDash \ mathtt { phi})
(M, g, w \ vDash \ mathtt {{ downarrow} a \ phi}) iff (M, g ', w \ vDash \ mathtt { phi}) kus (g') on (mathtt {a}) - (g) variant, et (g '(mathtt {a}) = w).
Valem (mathtt { phi}) öeldakse olevat tõene aadressil (w), kui (M, g, w \ vDash \ mathtt { phi}); vastasel juhul öeldakse, et see on (w) vale. Tavapäraselt tähendab (M, g \ vDash \ mathtt { phi}) (M, g, w \ vDash \ mathtt { phi}) iga elemendi (w) kohta (W) ja (M \ vDash \ mathtt { phi}) tähendab (M, g \ vDash \ mathtt { phi}) iga ülesande jaoks (g). Valem (mathtt { phi}) kehtib kaadris ainult siis, kui (M \ vDash \ mathtt { phi}) mis tahes mudeli (M) jaoks, mis põhineb kõnealusel raamil. Valem (mathtt { phi}) kehtib kaadriklassis (F) ainult siis, kui (mathtt { phi}) kehtib mis tahes kaadris rakenduses (F). Valem (mathtt { phi}) kehtib ainult siis, kui (mathtt { phi}) kehtib kõigi kaadrite klassis. Rahuldatavuse määratlus jääb lugejale.
Pange tähele, et sideaine (mathtt { downarrow}) on defineeritav järgmiselt: (mathtt { forall}) kui valem (mathtt {{ downarrow} a \ phi \ leftrightarrow \ forall a (a \ rightarrow \ phi)}) kehtib igas kaadris.
Seda, et tavalise modaalloogika hübridiseerimine tegelikult väljendusrikkama jõu annab, saab vaadelda näiteks valemiga (mathtt {{ downarrow} c \ Box \ neg c}). On lihtne kontrollida, kas see valem kehtib kaadris ainult siis, kui kaader on ebarefleksne. Seega saab ebarefleksivsust väljendada hübriid-loogilise valemiga, kuid on hästi teada, et seda ei saa väljendada tavalise modaalloogika ühegi valemiga. Ebarefleksivsust saab tegelikult väljendada lihtsalt nominaalide lisamisega tavalisele modaalloogikale, valemi (mathtt {c \ rightarrow \ Box \ neg c}) abil. Muud hübriidloogikas, kuid mitte tavalises modaalses loogikas väljendatavate omaduste näited on asümmeetria (väljendatud (mathtt {c \ parempoolne \ Box \ neg \ Diamond c})), antisümmeetria (väljendatud (mathtt { c \ parempoolne \ kast (Teemant c \ paremnool c)})),ja universaalsus (väljendatud numbriga (mathtt { Diamond c})).
Hübriidloogika süntaksi ja semantika, aga ka paljude muude põhimääratluste üksikasjaliku ülevaate leiate käsiraamatu peatükist Valdkonnad ja kümme Cate (2006). Ülaltoodud süntaksit ja semantikat saab laiendada mitmel viisil, eriti saab lisada esimese järgu masinaid (muidugi samaväärne viis esimese järgu hübriidloogika saamiseks on hübriidloogiliste masinate lisamine esimese järgu modaalidele) loogika). Esimese astme hübriidloogika ülevaate leiate Braünerist (2014), täpsema ülevaate leiate Braüneri (2011a) 6. peatükist ja esimese astme hübriidloogika integreeritud loogika kohta leiate peatükist Braüner (2011a) 7. peatükist.
3. Tõlked
Hübriidloogikat saab tõlkida võrdsusega esimese järgu loogikaks ja võrdsusega esimese järgu loogikat (fragmendi) tagasi hübriidloogikaks (fragmendiks). Vaadeldavatel esimese astme keeltel on 1-kohaline predikatsioonisümbol (mathtt {p ^ *}), mis vastab modaaloogika igale tavalisele alussümbolile (mathtt {p}), 2-kohaline predikatsioonisümbol (mathtt {R}) ja kahekohalise predikaadi sümbol (mathtt {=}). Muidugi tõlgendatakse predikatiivi sümbolit (mathtt {p ^ *}) nii, et see relativiseerib vastava modaalse algatussümboli (mathtt {p}) tõlgendamist maailmadesse, predikatiivi sümbolit (mathtt {R}) tõlgendatakse juurdepääsetavuse seose abil ja predikaat sümbolit (mathtt {=}) tõlgendatakse identiteetide seose abil maailmades. Andsime (mathtt {a}, \ mathtt {b},\ mathtt {c}, \ ldots) vahemik esimese järgu muutujate vahel. Keelel pole püsivaid või funktsioonisümbolid. Me tuvastame esimese astme muutujad hübriidloogika nominaalidega.
Esmalt tõlgime hübriidloogika võrdsusega esimese astme loogikaks. Arvestades kahte uut esimese järgu muutujat (mathtt {a}) ja (mathtt {b}), on tõlked (mathrm {ST} _ \ mathtt {a}) ja (mathrm { ST} _ \ mathtt {b}) määratletakse vastastikuse rekursiooniga. Anname lihtsalt tõlke (mathrm {ST} _ \ mathtt {a}).
(Mathrm {ST} _ \ mathtt {b}) määratlus saadakse vahetades (mathtt {a}) ja (mathtt {b}). Tõlge on tuntud standardtõlke laiendus modaalsest loogikast esimese järgu loogikasse. Näitena demonstreerime samm-sammult, kuidas hübriid-loogiline valem (mathtt {{ downarrow} c \ Box \ neg c}) teisendatakse esimese järgu valemiks:
Saadud esimese astme valem on samaväärne dokumendiga (mathtt { neg R (a, a)}), mis näitab, et (mathtt {{ downarrow} c \ Box \ neg c}) vastab tõepoolest ligipääsetavuse seos on ebarefleksne, vrd. ülalpool.
Esimese astme loogikat koos võrdsusega saab tõlkida tagasi hübriidloogikasse allpool toodud tõlke HT abil.
Pange tähele, et hübriid-loogilist sideainet (mathtt { forall}) on vaja. Ülalnimetatud tähelepanekute ajalugu ulatub tagasi Arthur N. Prior'i töö juurde, selle juurde naaseme hiljem.
Sarnaselt võib seda, mida nimetatakse esimese järgu loogika piiritletud fragmendiks, tõlkida hübriidloogikasse, kuid siin on vaja ainult sideainet (mathtt { downarrow}), nagu on märgitud paberites Areces, Blackburn ja Marx (2001). Piiratud fragment on esimese järgu loogika fragment omadusega, et kvantifitseerijad esinevad ainult nagu valemis (mathtt { forall c (R (a, c) rightarrow \ phi)}), kus see on vajalik et muutujad (mathtt {a}) ja (mathtt {c}) on erinevad. Tõlke piiritletud fragmendist hübriidloogikasse ilma (mathtt { forall}) sideaineta saab, asendades ülaltoodud tõlke HT viimase lause järgmisega:
) mathrm {HT} (mathtt { jätka c (R (a, c) parempoolne \ phi)}) = \ mathtt {@_ a \ Box { downarrow} c} mathrm {HT} (mathtt { phi}).)
Areces, Blackburn ja Marx (2001) annavad piiratud fragmendi jaoks mitu iseseisvat semantilist iseloomustust.
Ülaltoodud tõlked säilitavad tõde. Selle ametlikuks kinnitamiseks tuleb kasutada üldtuntud tähelepanekut, et hübriidloogika mudeleid ja ülesandeid võib käsitada esimese järgu loogika mudelitena ja määramisena ning vastupidi. Neid tõe säilitamise tulemusi on lihtne sõnastada ja jätame üksikasjad lugeja hooleks. Seega on hübriidloogikal koos sideainega (mathtt { forall}) sama ekspressiivne jõud kui esimese järku loogikal võrdsusega ja hübriidloogikal ilma sideaineta (mathtt { forall}) (kuid koos köitjal (mathtt { downarrow})) on sama väljendusjõud kui esimese järgu loogika piiritletud fragmendil (pange tähele, et tõlge (mathrm {ST} _ \ mathtt {a} (mathtt { phi})) suvalise valemiga (mathtt { phi}) ilma sideaineta (mathtt { forall}) on piiratud fragmendis).
Ülaltoodud tõlkeid saab laiendada esimese järgu hübriidloogikale, sel juhul on asjakohane sihtloogika kahesuguse võrdusega võrdsustatud esimese järgu loogika, üks sort maailmade jaoks ja üks sort indiviidide jaoks, vt Braüneri (2011a) 6. peatükk. Intensiivse esimese järgu hübriidloogika puhul kasutatakse kolme sorti, kolmas on intensiivsuste jaoks, vt Braüneri (2011a) 7. peatükki.
4. Arthur N. Eelnev ja hübriidloogika
Hübriidloogika ajalugu ulatub tagasi Arthur N. Priori hübriidpingeloogikasse, mis on tavalise pingelise loogika hübridiseeritud versioon. Selle edasise uurimise huvides anname hübriidse pingeloogika ametliku määratluse: hübriidse pingeloogika keel on lihtsalt ülalmääratletud hübriidloogika keel, välja arvatud see, et on kaks modaaloperaatorit, nimelt (mathtt {G}) ja (mathtt {H}), ühe modaalse operaatori (mathtt { Box}) asemel. Kahte uut transpordiliigi operaatorit nimetatakse pingelisteks operaatoriteks. Hübriidloogika semantika on hübriidloogika semantika, vrd. varem koos klausliga (mathtt { Box}) asendatud klauslitega pingelistele operaatoritele (mathtt {G}) ja (mathtt {H}).
(M, g, w \ vDash \ mathtt {G \ phi}) kui (W) mis tahes elemendi (v) korral on (wRv), siis on (M, g, v \ vDash \ mathtt { phi})
(M, g, w \ vDash \ mathtt {H \ phi}) iff iga elemendi (v) jaoks (W), nii et (vRw), juhtub nii, et (M, g, v \ vDash \ mathtt { phi})
Seega on nüüd kaks transpordiliigiga operaatorit, nimelt üks, kes "otsib edasi" mööda juurdepääsetavuse suhet ja teine, mis "vaatab tagasi". Pingelises loogikas nimetatakse hulga (W) elemente hetkedeks või hetkedeks ja seost (R) nimetatakse varasemaks-hilisemaks seoseks.
Muidugi on ülaltoodud tõlgete (mathrm {ST} _a) ja (mathrm {HT}) muutmine nii lihtne, et tõlked saadakse hübriidse pingeloogika vahel (sealhulgas (mathtt { forall }) sideaine) ja esimese astme loogika võrdsusega. Vaadeldav esimese järgu loogika on see, mida Prior nimetas esimese järgu varasemaks-hilisemaks loogikaks. Tõlkeid arvestades järeldub sellest, et Priori esimese järgu varasemal-hilisemal loogikal on sama väljendusjõud kui hübriidsel pingeloogikal.
Nüüd tutvustas Prior hübriidset pingeloogikat seoses sellega, mida ta nimetas pingeloogilise osaluse neljaks klassiks. Tema nelja pingelise loogilise kaasamise motivatsioon oli filosoofiline. Neli klassi olid esitatud raamatu Prior (1968) XI peatükis (ka XI peatükk uues väljaandes Prior (2003)). Vt lisaks eelnevat (1967), peatükk V.6 ja lisa B.3-4. Üldisema arutelu jaoks lugege postuumselt ilmunud raamatut „Enne ja peenike” (1977). Etapid liiguvad alates sellest, mida võib pidada puhtaks esimese järgu varasemaks-hilisemaks loogikaks, kuni puhta pingeloogikaks; eesmärk on osata neljanda etapi pingelist loogikat käsitleda esimese etapi varasemat-hilisemat loogikat hõlmavana. Teisisõnu, eesmärk oli suuta tõlkida varasema-hilisema seose esimese astme loogika pingeliseks loogikaks. Just seda eesmärki silmas pidades tutvustas Prior nn kiirpakkumisi:
See, mida ma nimetan pingeloogilise kaasamise kolmandaks astmeks, seisneb hetkemuutujate (a, b, c) jms käsitlemises, mis esindavad ka ettepanekuid. (Eelmine 2003, lk 124)
Modaalse loogika kontekstis nimetas Prior selliseid väiteid võimalikeks maailmapakkumisteks. Muidugi nimetatakse seda siin nominentideks. Enne tutvustas ka sideainet (mathtt { forall}) ja seda, mida me siin nimetame rahuloluoperaatoriteks (ta kasutas märke (mathtt {T (a, \ phi)}) asemel (mathtt {@ _a \ phi}) rahulolu operaatoritele). Tegelikult on Priori kolmanda klassi pingeloogika identne hübriidpingeloogikaga, nagu eespool määratletud. Sideaine (mathtt { downarrow}) võeti kasutusele palju hiljem. Nii omandas Prior oma esimese järjekorra varasema-hilisema loogika väljendusjõu, lisades tavalisele pingelisele loogikale veel väljendusjõudu nominaalide, rahuloluoperaatorite ja sideaine (mathtt { forall}) näol. Nii et tehnilisest küljest jõudis ta selgelt oma eesmärgini.
Filosoofilisest vaatepunktist on aga vaieldud selle üle, kas tema kolmanda astme pingelise loogika ontoloogiline import on sama, mis esimese järgu varasema-hilisema loogika ontoloogiline import. Näiteks peetakse mõne autori poolt ((mathtt { forall})) sideainet otseseks analoogiks esimese järgu (mathtt { forall}) kvantifikaatoriga ja on seetõttu kahtlane; vt näiteks Sylvani (1996) raamat kogumikus Copeland (1996). Samuti on asjakohased mitmed muud kogumiku artiklid. Priori neljanda klassi pingelise loogika arutelu leiate Braünerist (2002). Vt ka Øhrstrøm ja Hasle (1993), Øhrstrøm ja Hasle (2006), Müller (2007) ja Blackburn (2007). Lõpuks vaadake Priori nelja klassi arutelu Braüneri 1. peatükis (2011a).
Ülalnimetatud artiklis Øhrstrøm ja Hasle (2006) antakse üksikasjalik ülevaade Priori loogilisest tööst. Priori elu ja töö kohta saab põhjaliku ülevaate raamatust Øhrstrøm ja Hasle (1995). Raamatus Hasle ja Øhrstrøm (2016) kirjeldatakse Priori metoodilist lähenemist, eriti tema vaadet vormistamisele ja sümboolse loogika rollile kontseptuaalsetes uuringutes.
5. Hübriidloogika arendamine alates eelmisest
Hübriidloogika esimene täiesti range määratlus anti välja Bull (1970), mis ilmus ajakirja Theoria eriväljaandes Priori mälestuseks. Bull tutvustab kolmandat tüüpi algsümbolit, mille puhul eeldatakse, et algsümbol vastab hargnevas ajamudelis täpselt ühes harus (“sündmuste käik”). Seda ideed sortimissümbolite sorteerimiseks vastavalt nende tõlgendamise piirangutele on hiljem välja töötanud mitmed autorid, vt arutelu peatükis 5 Blackburn ja Tzakova (1999).
Hübriidloogilise masina, mille algselt leiutas Prior 1960. aastate lõpus, leiutasid 1980. aastatel Bulgaarias pärit Solomon Passy ja Tinko Tinchev, vt Passy ja Tinchev (1985), samuti Passy ja Tinchev (1991). Tavalise modaalloogika asemel toimus see töö seoses palju väljendusrikkama propositsioonilise dünaamilise loogikaga.
1990-ndatel aastatel oli suur panus köite kasutuselevõtt (mathtt { downarrow}). Valentin Goranko tutvustas allatõmbesideaine varajast versiooni artiklites Goranko (1994) ja Goranko (1996). Käesoleva töö versioon tutvustati Blackburnis ja Seligmanis (1995). Sellest ajast alates on põhjalikult uuritud sideaine (mathtt { downarrow}) hübriidloogikat, selle loogika mudelateoreetiliste aspektide kohta vt näiteks paberid Areces, Blackburn ja Marx (2001). Hübriidloogika mudelteooria põhjalik uurimine on kümne Cate'i (2004) doktoritöö.
Samuti on põhjalikult uuritud nõrgemat hübriidloogikat, mis on saadud, kui jätta välja mõlemad sideained (mathtt { downarrow}) ja (mathtt { forall}). Selgub, et see sideainevaba loogika ja mitmed selle variandid on otsustatavad. Ajakirjas Areces, Blackburn ja Marx (1999) on hübriidse modaalse ja pingelise loogika jaoks esitatud mitu keerukuse tulemust mitmesuguste kaadriklasside jaoks, näiteks suvalised, transitiivsed, lineaarsed ja hargnevad. On tähelepanuväärne, et sideainevaba hübriidloogika rahuldatavuse probleem suvaliste raamide korral on PSPACE-s lahendatav, mis on sama, mis tavalise modaalloogika korral rahuldatavuse otsustamise keerukus. Seega annab tavalise modaaloogika hübridiseerimine väljendusjõu, kuid keerukus jääb samaks. Mõningat tööd on tehtud nominaalainete simuleerimiseks modaalloogika sees,vt Kracht ja Wolter (1997).
Mis tahes tavaline modaalvalem väljendab kaadritel monaadilist teise järgu omadust ja on hästi teada, et mõne modaalvalemi, sealhulgas nn Sahlqvisti valemite korral võrdub teise järgu omadus esimese järgu omadusega. Raamatus Goranko ja Vakarelov (2006) on näidatud, et see kehtib ka hübriid-loogiliste valemite klassi, sealhulgas nominaalide kohta. Tavalise modaalvalemi esimese astme ekvivalentide arvutamiseks on mitu algoritmi. Üks selline algoritm, SQEMA, on artiklis Conradie, Goranko ja Vakarelov (2006), mis hõlmab ka Goranko ja Vakarelov (2006) käsitletud hübriid-loogilisi valemeid.
On tähelepanuväärne, et esimese astme hübriidloogika pakub täpselt neid funktsioone, mida on vaja interpolatsiooniteoreemide tõestamiseks: Kuigi interpolatsioon ebaõnnestub paljudes tuntud esimese astme modaalloogikates, on nende hübridiseeritud kolleegidel see omadus, vt Areces, Blackburn ja Marx (2003), samuti Blackburn ja Marx (2003). Esimene töö annab interpolatsiooni teoreetilise mudeli tõestuse, teine paber aga interpolantide arvutamise algoritmi tabelisüsteemi alusel.
Samuti tuleks mainida, et hübriidloogikaga sarnastel loogikatel on kirjeldusloogika valdkonnas keskne roll, mis on tehisintellekti teadmiste esitamiseks kasutatav loogikaperekond, vt artikleid Blackburn ja Tzakova (1998) ning Carlos Areces 'PhD lõputöö (2000).
Nagu eelmises osas kirjeldati, võttis Prior sisse hübriidse pingeloogika konkreetse teema käsitlemiseks ajafilosoofias, kuid Prior (1968) XIV peatükis (ka XIV peatükk uues väljaandes Prior (2003)) näitas ta ka et hübriidne pingeloogika võib asendada kahemõõtmelise ajalise loogika, mille Hans Kamp tutvustas Kampis (1971). Mõõt on lihtsalt nende valemite arv, mille suhtes valemit hinnatakse, seega võimaldab hübriid-loogilise masina lisamine asendada kaks mõõdet ühega. Sellele tööle on hiljuti järgitud paljudes artiklites Blackburn ja Jørgensen, ülevaate saamiseks vt Blackburn ja Jørgensen (2016a). Nüüd anname sellest tööliigist lühikese visandi, mis on kohandatud käesoleva töö terminoloogiaga. Vaatlusalusel hübriilloogika versioonil on määratud nominaalne (mathtt {nüüd}) ja iga mudel on koos määratud ajaga (t_0) nii, et i) igat iseseisvat valemit hinnatakse suhtega (t_0) ja ii) nominaalne (mathtt {nüüd}) tähistab (t_0). Ametlikumalt võtame kasutusele tava, et ((M, t_0), g \ vDash \ mathtt { phi}) tähendab (M, g, t_0 \ vDash \ mathtt { phi}) ja kaalume ainult ülesandeid (g) kus (g (mathtt {nüüd}) = t_0). Pange tähele, et nominaalne (mathtt {nüüd}), mida peetakse eraldiseisvaks valemiks, kehtib selles semantikas, kuid ühegi teise nominaali puhul see pole nii. Seda uut kehtivuse mõistet nimetavad Blackburn ja Jørgensen kontekstuaalseks kehtivuseks. Paber Blackburn ja Jørgensen (2013) annab aksioomisüsteemi, mis on täielik wrt. see kontekstuaalse kehtivuse mõiste. Paber Blackburn ja Jørgensen (2012) annab täieliku tabelisüsteemi, kuid selle paberi semantika on kooskõlas Kampi originaalse kahemõõtmelise semantikaga. Mõlemas lehes käsitletakse ka muid indekseerijaid nagu (mathtt {eile}), (mathtt {täna}) ja (mathtt {homme}).
Raamatus Blackburn ja Jørgensen (2016b) kasutatakse hübriidset pingeloogikat, et ühendada Priori ideed Hans Reichenbachi ideedega looduskeele pingete kirjeldamiseks. Eelistasid eelpool kirjeldatud tuntud pingelisi operaatoreid, samas kui Reichenbach eelistas ajalisi viiteid, see tähendab viiteid kindlatele aegadele, Reichenbach (1947). Selgub, et neid kahte lähenemisviisi saab kombineerida, mis ei olnud Priori enda valitud tee - vt Blackburnis ja Jørgensenis (2016b) esitatud aruannet,
6. Hübriidloogika aksioomid
Hübriidloogika aksioomidega on tegeletud paljudes artiklites, näiteks Gargov ja Goranko (1993), Blackburn (1993) ning Blackburn ja Tzakova (1999). Töös Gargov ja Goranko (1993) on esitatud hübriidloogika aksioomisüsteem ja näidatakse, et kui süsteemi laiendatakse täiendavate aksioomide komplektiga, mis on puhtad valemid (see tähendab, valemid, kus kõik algsümbolid on nominaalsed), siis on laiendatud aksioomide süsteem kõnesolevate aksioomide valideerimise klassi osas täielik. Puhtad valemid vastavad juurdepääsetavuse suhte esimese astme tingimustele (vt tõlge (mathrm {ST} _ \ mathtt {a})), seega uute hübriidloogika aksioomisüsteemid koos juurdepääsetavuse esimese järgu tingimustega Seose saab saada ühtlaselt, lisades vajadusel aksioome. Niisiis,Kui näiteks aksioomina lisada valem (mathtt {c \ parempoolne \ Box \ neg c}), siis on tulemuseks olev süsteem ebarefleksiaalsete kaadrite osas täielik, vrd. varem. Vt selliste reeglite arutelu ajakirja Blackburn (2000) 4. jaos.
Gargovi ja Goranko (1993) tõestussüsteem kasutab keerulist reeglit (nn COV), kus reegli aktiivset osa sisaldav valemiskeem võib olla suvaliselt suur; tegelikult on aktiivne osa manustatud modaaloperaatorite meelevaldselt sügavatesse pesadesse. Blackburn ja Tzakova (1999) näitavad, et rahuloluoperaatoritega saab aksioomisüsteemi formuleerida standardvormingus, kasutades lihtsamat reeglit nimega PASTE, nii et puhaste aksioonidega laiendatud süsteem on endiselt täielik.
Paber Blackburn ja kümme Cate (2006) uurivad ortodoksseid tõestuseeskirju (mis on tõendusreeglid ilma külgtingimusteta) aksioomisüsteemides ja näidatakse, et kui üks eeldab laiendatud täielikkust puhaste valemite abil, siis on ebatavalised tõestusreeglid hädavajalikud. sideainevaba hübriidloogika aksioomisüsteemides, kuid aksioomisüsteemi saab anda ainult tugevama hübriidloogika jaoks, sealhulgas (mathtt { downarrow}) sideaine ortodokssete tõendusreeglitega. Vaadake ka raamatut Braüner (2011a) hübriidloogika teise aksioomisüsteemi kohta, samuti intuitiivse hübriidloogika aksioomisüsteemide kohta ja Nelsoni parakonsistentse loogika N4 hübridisatsiooni kohta (võrrelge Costa ja Martinsiga (2016), kus vaadeldakse teist parakonsistentset hübriidloogikat). Intuitsioonilise hübriidloogika ülevaate võib leida Braünerist (2011b).
Paberites Areces, Blackburn, Huertas ja Manzano (2014) käsitletakse kõrgema järgu modaalloogika hübriid-loogilist versiooni (see tähendab modaalloogikat, mis on üles ehitatud Kiriku lihtsa tüüpide teooria kohale). Antakse aksioomisüsteemid ja tõestatakse, et nende täielikkus on wrt. Henkin-tüüpi semantika. Paber Blackburn, Huertas, Manzano ja Jørgensen (2014) laiendab neid tulemusi nii, et see hõlmab allanoole sidujat ning annab tõlkeid esimese astme loogika piiratud fragmendist ja sealt (vt eespool).
7. Hübriidloogika analüütilised tõestusmeetodid
Tableau, Gentzen ja loodusliku deduktiivsuse stiilis tõestusteooria hübriidloogika jaoks toimivad väga hästi, võrreldes tavalise modaalloogikaga. Tavaliselt, kui antakse modaalne tabel, Gentzen või naturaalne deduktsioonisüsteem, on see ühe konkreetse modaalloogika jaoks ja on osutunud problemaatiliseks moodustada sellised modaaloogika süsteemid ühtsel viisil ilma metalingvistilisi masinaid juurutamata. Seda saab parandada hübridiseerimisega, see tähendab, et modaalloogika hübridiseerimine võimaldab formuleerida ühtsed tabelid, Gentzen ja looduslikud deduktiivsüsteemid paljude loogikaklasside jaoks. Paber Blackburn (2000) tutvustab hübriilloogika tabelisüsteemi, millel on see soovitav omadus: Analoogselt Blackburn ja Tzakova (1999) aksioomisüsteemile säilib täielikkus, kui tabelisüsteemi laiendatakse puhaste aksioomide komplektiga, see tähendab,puhaste valemite komplekt, mida on lubatud tabelisse ehitamise ajal lisada. Blackburn (2000) tabelisüsteem on aluseks otsustusprotseduurile hübriidloogika sidujavaba fragmendi kohta, mis on välja antud Bolanderis ja Braüneris (2006). Seda tööd jätkati artiklites Bolander ja Blackburn (2007) ning Bolander ja Blackburn (2009). Raamatus Cerrito ja Cialdea (2010) on esitatud veel üks hübriilloogika tabelipõhine otsustusprotseduur. Muud hübriidloogika otsustusprotseduurid, mis samuti põhinevad tõestusteoorial, on toodud artiklis Kaminski ja Smolka (2009). Viimase paberi protseduurid põhinevad hübriidloogika kõrgema järgu formuleerimisel, mis hõlmab lihtsalt trükitud lambda-arvutust. Blackburn (2000) tabelisüsteem on aluseks otsustusprotseduurile hübriidloogika sidujavaba fragmendi kohta, mis on välja antud Bolanderis ja Braüneris (2006). Seda tööd jätkati artiklites Bolander ja Blackburn (2007) ning Bolander ja Blackburn (2009). Raamatus Cerrito ja Cialdea (2010) on esitatud veel üks hübriilloogika tabelipõhine otsustusprotseduur. Muud hübriidloogika otsustusprotseduurid, mis samuti põhinevad tõestusteoorial, on toodud artiklis Kaminski ja Smolka (2009). Viimase paberi protseduurid põhinevad hübriidloogika kõrgema järgu formuleerimisel, mis hõlmab lihtsalt trükitud lambda-arvutust. Blackburn (2000) tabelisüsteem on aluseks otsustusprotseduurile hübriidloogika sidujavaba fragmendi kohta, mis on välja antud Bolanderis ja Braüneris (2006). Seda tööd jätkati artiklites Bolander ja Blackburn (2007) ning Bolander ja Blackburn (2009). Raamatus Cerrito ja Cialdea (2010) on esitatud veel üks hübriilloogika tabelipõhine otsustusprotseduur. Muud hübriidloogika otsustusprotseduurid, mis samuti põhinevad tõestusteoorial, on toodud artiklis Kaminski ja Smolka (2009). Viimase paberi protseduurid põhinevad hübriidloogika kõrgema järgu formuleerimisel, mis hõlmab lihtsalt trükitud lambda-arvutust. Seda tööd jätkati artiklites Bolander ja Blackburn (2007) ning Bolander ja Blackburn (2009). Raamatus Cerrito ja Cialdea (2010) on esitatud veel üks hübriilloogika tabelipõhine otsustusprotseduur. Muud hübriidloogika otsustusprotseduurid, mis samuti põhinevad tõestusteoorial, on toodud artiklis Kaminski ja Smolka (2009). Viimase paberi protseduurid põhinevad hübriidloogika kõrgema järgu formuleerimisel, mis hõlmab lihtsalt trükitud lambda-arvutust. Seda tööd jätkati artiklites Bolander ja Blackburn (2007) ning Bolander ja Blackburn (2009). Raamatus Cerrito ja Cialdea (2010) on esitatud veel üks hübriilloogika tabelipõhine otsustusprotseduur. Muud hübriidloogika otsustusprotseduurid, mis samuti põhinevad tõestusteoorial, on toodud artiklis Kaminski ja Smolka (2009). Viimase paberi protseduurid põhinevad hübriidloogika kõrgema järgu formuleerimisel, mis hõlmab lihtsalt trükitud lambda-arvutust. Viimase paberi protseduurid põhinevad hübriidloogika kõrgema järgu formuleerimisel, mis hõlmab lihtsalt trükitud lambda-arvutust. Viimase paberi protseduurid põhinevad hübriidloogika kõrgema järgu formuleerimisel, mis hõlmab lihtsalt trükitud lambda-arvutust.
Artiklis Hansen, Bolander ja Braüner (2017) antakse tabelina põhinev otsustusprotseduur paljude väärtustega hübriidloogika jaoks, see tähendab hübriidloogika jaoks, kus kahe väärtusega klassikaline loogikabaas on üldistatud mitme väärtusega loogikabaasiks, mis hõlmab tõe-väärtusruum, millel on piiratud Heytingi algebrani struktuur. Hansen (2010) annab tabelipõhise otsustusprotseduuri dünaamilise episteemilise loogika hübridiseeritud versiooni jaoks, mida nimetatakse avaliku annouction-loogikaks. See on ka doktoritöö Hansen (2011) suur teema.
Hübriidloogika looduslikku deduktsioonistiili tõestusteooriat on uuritud raamatus Braüner (2011a). See raamat annab hübriilloogika jaoks ka Gentzeni süsteemi. Neid looduslike deduktsioonide ja Gentzeni süsteeme saab laiendada täiendavate tõendusreeglitega, mis vastavad nn geomeetriliste teooriatega väljendatud juurdepääsetavussuhete esimese astme tingimustele (see on muidugi analoogne puhaste aksioomidega laiendatud tabelite ja aksioomide süsteemidele). Vt ka Braüner ja de Paiva (2006), kus intuitiivse hübriidloogika jaoks antakse loomulik deduktsioonisüsteem (Braüneri (2011a) 8. peatükk).
Esimese astme hübriidloogika tabelisüsteeme võib leida artiklitest Blackburn ja Marx (2002). Esimese järgu hübriidloogika loomulikke deduktsioone ja aksioomisüsteeme võib leida raamatu Braüner (2011a) 6. peatükist ja raamatu 7. peatükis käsitletakse esimese astme hübriidloogika loomuliku deduktsiooni jaoks. Raamatus Barbosa, Martins ja Carreteiro (2014) antakse esimese astme hübriidloogika fragmendi aksiomatization, mida nimetatakse võrdsustatud esimese järgu hübriidloogikaks.
Hübriidloogikaga sarnaseid loogika õrnaid ja looduslikke deduktiivsüsteeme uuris Jerry Seligman juba 1990. aastatel, vt ülevaadet ajakirjas Seligman (2001). Eelkõige töötas Seligman välja tõestussüsteemid, mis töötavad meelevaldsete valemitega, mitte ainult rahulolu avaldustega, viimane kehtib enamiku hübriidloogika tõestussüsteemide kohta, kus rahulolukorraldajaid kasutatakse modaalsuste taha peidetud teabele juurdepääsuks. Seligmanis looduslik deduktsioonisüsteem võeti kasutusele Seligmanis (1997) ja seda süsteemi on edasi arendatud raamatu Braüner (2011a) 4. peatükis. Seligmani korrektses stiilis tabelisüsteeme on kaalutud Blackburnis, Bolanderis, Braüneris ja Jørgensenis (2017), kus antakse süntaktiline täielikkuse tõend. Seminaarne täielik tõend tabelisüsteemi kohta on antud Jørgensenis, Blackburnis, Bolanderis,Braüner (2016). Nende süsteemide mõttekäik ei tugine otseselt globaalsetele kodeeringutele, mille rahuloluoperaatorid võimaldavad, seega võib neid süsteeme pidada rohkem vastavaks Kripke'i modaaloogika semantika kohalikule iseloomule. Tegelikult muudab see lokaalsem mõttekäik need süsteemid sobivaks teatud psühholoogilistes mõttekäikudes toimuva perspektivisaalse mõttekäigu vormistamiseks, vt nii Braüner (2014b) kui ka Braüner, Blackburn ja Polyanskaya (2016).see lokaalsem arutlusstiil muudab need süsteemid sobivaks teatud psühholoogilistes mõttekäikudes toimuva perspektiiva mõtlemise vormistamiseks, vt Braüner (2014b), aga ka Braüner, Blackburn ja Polyanskaya (2016).see lokaalsem arutlusstiil muudab need süsteemid sobivaks teatud psühholoogilistes mõttekäikudes toimuva perspektiiva mõtlemise vormistamiseks, vt Braüner (2014b), aga ka Braüner, Blackburn ja Polyanskaya (2016).
Mõnda tööd on tehtud eraldusvõimekivi ja mudeli kontrollimise osas, vt eraldusvõime kalkulatsioonide kohta Areces, de Rijke ja de Nivelle (2001) ning samuti Areces ja Gorin (2011) ning vt Franceschet ja de Rijke (2006), samuti Lange (2009) mudeli kontrollimise tulemuste kohta.
Alates 1990ndate keskpaigast on hübriidloogikaga seotud tööd õitsenud. Täiendavate viidete saamiseks viitame lugejale bibliograafias avaldatud väljaannetele. Lisaks vaadake allpool Interneti-ressursse.
Bibliograafia
Areces, C., 2000. Loogikatehnika. Kirjelduse ja hübriidloogika juhtum, doktoritöö, loogika, keele ja arvutuse instituut, Amsterdami ülikool.
Areces, C., Blackburn, P. ja Marx, M., 1999. “Hübriidse ajaloogika arvutuslik keerukus”, IGPLi loogikaajakiri, 8: 653–679.
–––, 2001. “Hübriidloogika: iseloomustus, interpolatsioon ja keerukus”, Journal of Symbolic Logic, 66: 977–1010.
––– 2003. “Interpolatsiooniteoreemi parandamine kvantifitseeritud modaalloogikas”, Annals of Puhas ja rakendatud loogika, 124: 287–299.
Areces, C., Blackburn, P., Huertas, A. ja Manzano, M., 2014. “Täielikkus hübriidtüübi teoorias”, Journal of Philosophical Logic, 43: 209–238.
Areces, C., de Rijke, M., ja de Nivelle, H., 2001. “Resolution in Modal, Description and Hybrid Logic”, Journal of Logic and Computation, 11: 717–736.
Areces, C. ja Gorin, D., 2011. “Hübriidloogika lahendamine koos valiku ja valikuga”, Journal of Automated Reasoning, 46: 1–42.
Areces, C. ja kümme Cate, B., 2006. “Hybrid Logics”, Blackburn, van Benthem ja Wolter (toim) (2006).
Barbosa, LS, Martins, MA ja Carreteiro, M., 2014. “Hilbert-Style Axiomatisation for Equational Hybrid Logic”, ajakiri Logic, Language and Information, 23: 31–52.
–––, 2000. “Märgistatud mahaarvamise sisestamine”, Journal of Logic and Computation, 10: 137–168.
–––, 2007. “Arthur Prior ja hübriidloogika”, Synthese, 150: 329–372.
Blackburn, P., Bolander, T., Braüner, T. ja Jørgensen, KF, 2017. “Seligmani stiilis tabelisüsteemi täielikkus ja lõpetamine”, ajakiri Logic and Computation, 27: 81–107.
Blackburn, P., Huertas, A., Manzano, M. ja Jørgensen, KF, 2014. “Henkin ja hübriidloogika”, Leon Henkini elus ja töös: Esseed tema kaastöödest (Studies in Universal Logic), lk 279–306. Birkhäuser.
Blackburn, P. ja Jørgensen, KF, 2012. „Indekseeritud hübriidne pingeloogika”, ajakirjas Advances in Modal Logic (9. köide), lk 144–160. Kolledžite väljaanded.
–––, 2016b. “Reichenbach, eelnev ja hübriidne pingeloogika”, Synthese, 193: 3677–3689.
Blackburn, P. ja Marx, M., 2002. “Tableaux for Quantified Hybrid Logic”, automatiseeritud põhjendamises analüütilise Tableauxi ja sellega seotud meetoditega, TABLEAUX (loengu märkused tehisintellekti osas: köide 2381), lk 38–52. Heidelberg: Springer.
Bolander, T. ja Braüner, T., 2006. “Hübriidloogika tabelipõhised otsustusprotseduurid”, Journal of Logic and Computation, 16: 737–763.
Braüner, T., 2002. “Modaalne loogika, tõde ja peamine modaalsus”, Journal of Philosophical Logic, 31: 359–386.
–––, 2011a. Hübriidloogika ja selle tõestusteooria (rakendatud loogika seeria: Köide 37), Dordrecht-Heidelberg-Berliin-New York: Springer.
–––, 2011b. “Intuitionistlik hübriidloogika: sissejuhatus ja uuring”, teave ja arvutused, 209: 1437–1446.
–––, 2014a. “Esimese astme hübriidloogika: sissejuhatus ja uuring”, IGPLi loogikaajakiri, 22: 155–165.
–––, 2014b. “Hübriid-loogiline mõttekäik nutitelefonides ja Sally-Anne ülesannetes”, ajakiri Logic, Language and Information, 23: 415–439.
Braüner, T., Blackburn, P., ja Polyanskaya, I., 2016. “Teise astme valeveendumuste ülesanded: analüüs ja vormistamine”, loogika, keele, teabe ja arvutuse alal: 23. rahvusvaheline töötuba, WoLLIC (loengu märkused arvutiteaduses: köide 9803), lk 125–144. Heidelberg: Springer.
Braüner, T. ja de Paiva, V., 2006. “Intuitionistic hübriidloogika”, Journal of Applied Logic, 4: 231–255.
Bull, R., 1970. “Lähenemisviis pingelisele loogikale”, Theoria, 36: 282–300.
Cerrito, S. ja Cialdea, M., 2010. “Nominaalne asendamine töös globaalse ja vastupidise modaalsusega”, Advances in Modal Logic (8. köide), lk 57–74. Kolledžite väljaanded.
Conradie, W., Goranko, V., ja Vakarelov, D., 2006. “Algoritmiline kirjavahetus ja täielikkus modaalses loogikas II. Algoritmi SQEMA polüadilised ja hübriidsed laiendid”, Journal of Logic and Computation, 16: 579–612.
Copeland, J. (toim.), 1996. Loogika ja reaalsus: Esseed Arthur Priori pärandis, Oxford: Clarendon Press.
Costa, D. ja Martins, MA, 2016. Ilmub ajakiri Logic and Computation “Parakonsistents hübriidloogikas”. DOI:
Franceschet, M. ja de Rijke, M., 2006. “Hübriidloogika kontrollimise mudel (koos rakendusega poolstruktureeritud andmetele)”, Journal of Applied Logic, 4: 279–304.
Gabbay, D. ja Woods, J. (toim.), 2006. Loogika ja modaalsused kahekümnendal sajandil. Loogika ajaloo käsiraamat (7. köide). Amsterdam: Elsevier.
Gargov, G. ja Goranko, V., 1993. “Modaalloogika nimedega”, Journal of Philosophical Logic, 22: 607–636.
Goranko, V., 1994. “Ajaline loogika koos viidetega”, ajalise loogika 1. rahvusvahelise konverentsi toimetistes (loengu märkused tehisintellekti osas: köide 827), lk 133–148. Berliin: Springer.
–––, 1996. “Modaalse ja ajalise loogika hierarhiad viidetega”, Journal of Logic, Language and Information, 5: 1–24.
Goranko, V. ja Vakarelov, D., 2001. “Sahlqvisti valemid hübriidse polüadi modaalses loogikas”, ajakiri Logic and Computation, 11: 737–754.
–––, 2011. Loogika tööriistakast teadmiste ja teabe modelleerimiseks mitme agendi süsteemides ja sotsiaalses epistemoloogias, doktoritöö, Roskilde ülikool.
Hansen, JU, Bolander, T., ja Braüner, T., 2015. Ilmub ajakiri Logic and Computation “Paljud väärtustatud hübriidloogika”. DOI:
Hasle, P. ja Øhrstrøm, P., 2016. “Priori paradigma aja uurimiseks ja selle metoodilisteks motivatsioonideks”, Synthese, 193: 3401–3416.
Jørgensen, KF, Blackburn, P., Bolander, B. ja Braüner, T., 2016. “Seligmani stiilis Tableau süsteemide sünteetilised terviklikkuse tõendid”, ajakirjas Advances in Modal Logic (11. köide), lk 302–321. Kolledžite väljaanded.
Kaminski, M. ja Smolka, G., 2009. “Erineva ja vastupidise hübriilloogika lõppsüsteemide lõpetamine”, ajakiri Logic, Language and Information, 18: 437–464.
Passy, S. ja Tinchev, T., 1991. “Essee kombineeritud dünaamilises loogikas”, teave ja arvutus, 93: 263–332.
Enne AN, 1967. Minevik, olevik ja tulevik, Oxford: Clarendon Press.
–––, 1968. Papers on Time and Tense, Oxford: Clarendon Press.
–––, 2003. Papers on Time and Tense, Oxford: Oxford University Press. Priori teine muudetud ja laiendatud väljaanne (1968). Toimetanud P. Hasle, P. Øhrstrøm, T. Braüner ja J. Copeland.
Enne AN ja Fine, K., 1977. Worlds, Times and Selves, London: Duckworth. Põhineb Priori eessõna käsikirjadel ja K. Fine postitusel.
Reichenbach, H., 1947. Sümboolse loogika elemendid, New York: Free Press.
Seligman, J., 1997. “Õige kirjeldamise loogika”, “Advances in Intensional Logic” (Rakendatud loogika seeria: 7. köide), lk 107–135. Kluwer.
Seligman, J., 2001. “Internalisation: The hübriidloogika juhtum”, Journal of Logic and Computation, 11: 671–689.
Sylvan, R., 1996. “Muud aja närtsinud kännud”, Copeland (1996), lk 111–130.
ten Cate, B., 2004. Amsterdami ülikooli laiendatud modaalkeelte näidisteooria, doktoritöö, loogika, keele ja arvutuse instituut.
Akadeemilised tööriistad
sep mehe ikoon
Kuidas seda sissekannet tsiteerida.
sep mehe ikoon
Vaadake selle sissekande PDF-versiooni SEP-i sõprade veebisaidil.
info ikoon
Otsige seda sisenemisteema Interneti-filosoofia ontoloogiaprojektilt (InPhO).
phil paberite ikoon
Selle kande täiustatud bibliograafia PhilPapersis koos linkidega selle andmebaasi.
