Szukam artykułów i artykułów na temat modalnej logiki podstrukturalnej - nie na semantykę modalności logicznej liniowej, ale na logikę podstrukturalną wzbogaconą standardowymi operatorami modalnymi, np. Podstrukturalną K (coś w rodzaju MALL z operatorem skrzynki, koniecznością i regułami K).
Odpowiedzi:
Wiem o pracy polegającej na dodawaniu modalności czasowych do logiki liniowej w celu uzyskania czegoś, co nazywa się logiką czasową liniową (w przeciwieństwie do LTL = liniowa logika czasowa). Jest to dość ciekawe: formuła (bez modalności) jest interpretowana jako środków będących dostępne teraz . Następna modalności jest interpretowana jako zasoby dostępne w następnym kroku czasowym. Modalność skrzynki oznacza, że zasoby mogą zostać zużyte w dowolnym momencie w przyszłości, określone przez posiadacza zasobów , natomiast oznacza, że zasoby mogą zostać zużyte w dowolnym momencie określonym przez system◻ -. Zwróć uwagę na dualność między posiadaczem zasobu a systemem.
Banbara, M., Kang, K.-S., Hirai, T., Tamura, N .: Programowanie logiki we fragmencie intuicyjnej czasowej logiki liniowej . W: Codognet, P. (red.) ICLP 2001. LNCS, vol. 2237, s. 315–330. Springer, Heidelberg (2001)
Hirai, T .: Propozycyjna logika czasowa liniowa i jej zastosowanie w systemach współbieżnych . Transakcje EICE dotyczące podstaw elektroniki, komunikacji i informatyki (sekcja specjalna na temat technologii systemów współbieżnych) E83-A (11), 2219–2227 (2000)
Hirai, T .: Temporalna logika liniowa i jej zastosowanie . Praca doktorska, The Graduate School of Science and Technology, Kobe University, Japonia (wrzesień 2000).
Kamide, N .: Temporalizing Linear Logic Bulletin of the Section of Logic Volume 36: 3/4 (2007), s. 173–182
Istnieje kilka artykułów, które dodają różnego rodzaju modalności do logiki liniowej i afinicznej:
Kamide, N .: Logika liniowa i afiniczna z logiką czasową, przestrzenną i epistemiczną . Theoretical Computer Science 252, 165–207 (2006).
Kamide, N: Łącząc miękką logikę liniową i operatory czasoprzestrzenne . J Logic Computation (2004) 14 (5): 625-650.
Prace nad czasową logiką liniową zostały zastosowane w programowaniu i koordynacji zorientowanej na agenta, wykorzystując istotnie interpretację opisanych powyżej modalności:
Kungas, P .: Tymczasowa logika liniowa do symbolicznej negocjacji agenta . W: Zhang, C., W. Guesgen, H., Yeap, W.-K. (red.) PRICAI 2004. LNCS, vol. 3157, s. 23–32. Springer, Heidelberg (2004)
Pham, DQ, Harland, J., Winikoff, M .: Wybory agenta modelowania w czasowej logice liniowej . W: Baldoni, M., Son, TC, van Riemsdijk, MB, Winikoff, M. (red.) DALT 2007. LNCS, vol. 4897, s. 140–157. Springer, Heidelberg (2008)
Clarke, D. Koordynacja: Reo, Nets and Logic . Postępowanie FMCO, LNCS, vol. 5382. (2008)
Tego rodzaju logikę rozważa się w językoznawstwie: możesz zajrzeć do artykułu Michaela Moortgata, Categorial Type Logic .
! Modalnością logiki liniowej jest operator skrzynkowy spełniający aksjomaty S4.
Powszechnie wiadomo, że wyjątkowości! A nie można wyprowadzić - to znaczy, jeśli masz czerwony huk i niebieski huk, z których oba osobno spełniają zasady huku, nie możesz udowodnić, że są one równoważne. Nie przypominam sobie od razu, gdzie można znaleźć ten wynik, ale prawdopodobnie jest to w pracy Girarda z 1987 roku na temat logiki liniowej.
EDYCJA: Zapytałem Jasona Reeda, którego teza dotyczyła kodowania logiki liniowej w logikę hybrydową, i wskazał mi następujący artykuł Chaudhuri i Despeyroux, „A Logic for Constrained Process Calculi with Applications to Molecular Biology” . Rozszerzają intuicyjną logikę liniową z adnotacjami hybrydowymi, mającymi na celu odzwierciedlenie logiki czasowej, i wykonali bardzo czystą robotę - dowodzą nie tylko eliminacji cięć, ale także fokulacji. Wygląda więc na to, że uproszczenie rachunku różniczkowego i otrzymanie modalnego K a la Simpson powinno być proste.
Obecnie najbardziej systematyczną teorią dowodową, która pozwala na ułożenie wielu logiki modalnej na wielu logikach podstrukturalnych, jest logika wyświetlania Belnap, która została porządnie potraktowana przez Marcusa Krachta - zobacz w szczególności jego Moc i Słabość Modalnej Logiki Wyświetlania , 1996 - i Heinrich Wansing, Displaying Modal Logic , 1998.
Logika wyświetlania ma problemy z obsługą logiki nieprzemiennej, co było jedną z motywacji kilku prac magisterskich, które nadzorowałem kilka lat temu, do zastosowania pewnych pomysłów dotyczących reprezentowania modalności w rachunku różniczkowym, który jest bardzo silny do reprezentowania logiki podstrukturalnej, ale został uruchomiony w problemy ze względu na nietypowy sposób, w jaki udowodniono eliminację cięć. Praca Roberta Heina nad generowaniem reguł dla logiki modalnej z rodzin aksjomatów, streszczona w Czystości poprzez odkrywanie, 2005, obejmuje większość zwykłych logiki (najważniejsze nie uwzględnione aksjomaty to B, CR i L), i istnieją dość mocne dowody poszlakowe, aby wierzyć w hipotezę eliminacji cięcia. Żadna z tych prac nie traktuje logiki podstrukturalnej, ale gdyby udowodniono silniejsze twierdzenie o eliminacji cięć dla tych modalności, tak zwany lemat podziału, to uczyniłoby to logikę bardzo modularną, a eliminacja cięć powinna być łatwa dla wszystkich sposobów sklejenie logiki.
Logika podstrukturalna tak naprawdę nie ma jednolitego pojęcia semantyki, ale w przypadku modalnej logiki podstrukturalnej mamy pewien przepis na przekształcenie semantyki logiki podstawowej w semantykę dopasowywania logiki modalnej poprzez rozszerzenie semantyki podobnej do śladu z pojęciem ramka lub semantyka algebraiczna / kategoryczna z pojęciem operatora. Kracht i Wansing wykonują prace w obu tych kierunkach.
Szukałem Norihiro Kamide, „Kripke Semantics for Modal Substructural Logics”, Journal of Logic, Language and Information 11 (4) , 2002, co nie jest dokładnie tym, czego chciałem, ale odniesienia cytują Marcello D'Agostino i Dov M. Gabbay i Alessandra Russo, „Przeszczepianie modalności na podstrukturalne systemy implikacyjne”, Studia Logica 59 , 1996, która wydaje się być tym, czego szukam. Jest na CiteSeer http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.5719