Auf der Suche nach Aufsätzen und Artikeln zur Modal Substructural Logics

Ich bin auf der Suche nach Artikeln und Artikeln über modale Substrukturlogiken - nicht über die Semantik linearer Logikmodalitäten, sondern über Substrukturlogiken, die mit standardmäßigen Modaloperatoren, z.

Ich kenne Arbeiten, die der linearen Logik zeitliche Modalitäten hinzufügen, um eine sogenannte zeitliche lineare Logik zu erzeugen (im Gegensatz zu LTL = zeitliche Logik in linearer Zeit). Das ist sehr interessant: Eine Formel (ohne Modalität) wird so interpretiert, als stünden jetzt Ressourcen zur Verfügung . Die nächste wird als Ressourcen interpretiert, die im nächsten Zeitschritt verfügbar sind. Die Box-Modalität bedeutet, dass die Ressourcen zu jedem vom Inhaber der Ressourcen festgelegten Zeitpunkt in der Zukunft verbraucht werden können , während bedeutet, dass die Ressourcen zu jedem vom System festgelegten Zeitpunkt verbraucht werden können$\bigcirc-$$\Box-$$\lozenge-$. Beachten Sie die Dualität zwischen dem Inhaber der Ressource und dem System.

• M. Banbara, K.-S. Kang, T. Hirai, N. Tamura: Logikprogrammierung in einem Fragment der intuitionistischen zeitlichen linearen Logik . In: Codognet, P. (Hrsg.) ICLP 2001. LNCS, vol. 2237, S. 315–330. Springer, Heidelberg

• Hirai, T .: Propositionale zeitliche lineare Logik und ihre Anwendung auf gleichzeitige Systeme . EICE-Transaktionen zu Grundlagen der Elektronik, Kommunikation und Informatik (Sonderteil Concurrent Systems Technology) E83-A (11), 2219–2227 (2000)

• Hirai, T .: Zeitliche lineare Logik und ihre Anwendung . Doktorarbeit, The Graduate School für Wissenschaft und Technologie, Kobe University, Japan (September 2000).

• Kamide, N .: Temporalizing Linear Logic Bulletin des Abschnitts von Logic Volume 36: 3/4 (2007), S. 173–182

Es gibt einige Veröffentlichungen, die der linearen und affinen Logik alle möglichen Modalitäten hinzufügen:

• Kamide, N .: Lineare und affine Logik mit zeitlicher, räumlicher und epistemischer Logik . Theoretical Computer Science 252, 165–207 (2006).

• Kamide, N: Kombination von weichen linearen Logik- und räumlich-zeitlichen Operatoren . J Logic Computation (2004) 14 (5): 625 & ndash; 650.

Die Arbeit an der zeitlichen linearen Logik wurde in der agentenorientierten Programmierung und Koordination angewendet, wobei die Interpretation der oben beschriebenen Modalitäten wesentlich genutzt wurde:

• Kungas, P .: Zeitlineare Logik für die Verhandlung symbolischer Agenten . In: Zhang, C., W. Guesgen, H., Yeap, W.-K. (Hrsg.) PRICAI 2004. LNCS, vol. 3157, S. 23–32. Springer, Heidelberg

• Pham, DQ, Harland, J., Winikoff, M .: Auswahl des Modellierungsagenten in zeitlich linearer Logik . In: Baldoni, M., Sohn, TC, van Riemsdijk, MB, Winikoff, M. (Hrsg.) DALT 2007. LNCS, vol. 4897, S. 140–157. Springer, Heidelberg (2008)

• Clarke, D. Koordination: Reo, Netze und Logik . FMCO procedure, LNCS, vol. 5382. (2008)

Diese Art von Logik wird in der Linguistik betrachtet: Sie können sich Michael Moortgats Artikel Categorial Type Logic ansehen .

Die! A-Modalität der linearen Logik ist ein Kästchenoperator, der die S4-Axiome erfüllt.

Es ist bekannt, dass die Einzigartigkeit von! A nicht herleitbar ist. Wenn Sie also einen roten und einen blauen Paukenschlag haben, die beide die Regeln für Paukenschlag erfüllen, können Sie nicht beweisen, dass sie gleichwertig sind. Ich erinnere mich nicht ohne weiteres, wo dieses Ergebnis zu finden ist, aber es ist wahrscheinlich in Girards 1987er Arbeit über lineare Logik.

BEARBEITEN: Ich habe Jason Reed befragt, in dessen Diplomarbeit es um Codierungen linearer Logik in hybride Logik ging, und er hat mich auf den folgenden Aufsatz von Chaudhuri und Despeyroux hingewiesen: "Eine Logik für eingeschränkte Prozesskalküle mit Anwendungen auf die Molekularbiologie" . Sie erweitern die intuitionistische lineare Logik um hybride Annotationen, die die zeitliche Logik widerspiegeln sollen, und sie haben sehr gute Arbeit geleistet. Es sieht also so aus, als ob es einfach sein sollte, ihre Rechnung zu vereinfachen, um modales K a la Simpson zu erhalten.

Derzeit ist die systematischste Beweistheorie, mit der viele Modallogiken auf viele Substrukturlogiken aufgeschichtet werden können, die Anzeigelogik von Belnap, die von Marcus Kracht in angemessener Weise behandelt wurde - insbesondere seine Leistungsfähigkeit und Schwäche der Modaldisplaylogik . 1996 - und Heinrich Wansing, Viewing Modal Logic , 1998.

Die Darstellungslogik hat Probleme mit der Handhabung der nicht-kommutativen Logik, die eine der Beweggründe für einige MSc-Arbeiten war, die ich vor einigen Jahren betreut habe, um einige Ideen zur Darstellung von Modalitäten in der Strukturberechnung anzuwenden, die für die Darstellung von Substrukturlogiken sehr leistungsfähig ist, aber ausgeführt wurde in Probleme, weil die ungewöhnliche Art der Schnitteliminierung in dieser Einstellung bewiesen ist. Robert Heins Arbeit zur Generierung von Regeln für die Modallogik aus Axiomfamilien, zusammengefasst in Reinheit durch Enträtseln, 2005, deckt die meisten der üblichen Logiken ab (die wichtigsten nicht behandelten Axiome sind B, CR und L), und es gibt ziemlich starke Indizien dafür, dass die Vermutung der Schnitteliminierung angenommen wird. Keine dieser Arbeiten befasst sich mit der Substrukturlogik, aber wenn für diese Modalitäten eine stärkere Art von Cut-Elimination-Theorem, das sogenannte Splitting-Lemma, bewiesen würde, würde dies die Logik sehr modular machen und die Cut-Elimination sollte auf alle Arten leicht folgen können Zusammenkleben der Logik.

Substrukturelle Logik hat nicht wirklich einen einheitlichen Begriff der Semantik, aber für die modale substrukturelle Logik haben wir eine Art Rezept, um die Semantik der Basislogik in eine Semantik der übereinstimmenden modalen Logik umzuwandeln, indem eine spurenartige Semantik um den Begriff von erweitert wird Frame oder eine algebraische / kategoriale Semantik mit Operatorbegriff. Kracht und Wansing arbeiten in beide Richtungen.

Ich habe Norihiro Kamide, "Kripke Semantics for Modal Substructural Logics", Journal of Logic, Language and Information 11 (4) , 2002, überflogen, was nicht ganz das ist, was ich wollte, aber die Referenzen zitieren Marcello D'Agostino und Dov M. Gabbay und Alessandra Russo, "Transplantation von Modalitäten auf substrukturelle Implikationssysteme", Studia Logica 59 , 1996, was ich anscheinend suche. Es ist auf CiteSeer http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.5719