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

15

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.

rauben
quelle

Antworten:

13

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---. Beachten Sie die Dualität zwischen dem Inhaber der Ressource und dem System.

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

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:

Dave Clarke
quelle
8

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

Noam Zeilberger
quelle
8

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.

Neel Krishnaswami
quelle
1
Ich suche etwas Schwächeres, das eher K als S4 entspricht.
Rob
1
@Rob: Einige schwächere Modalitäten für die lineare Logik werden in der linearen Lichtlogik untersucht. Ich habe ein Papier gesehen, in dem die Beziehung zwischen drei LLLs und Standard-Kripkean-Modallogiken skizziert ist, aber ich vergesse, welche und ob K unter ihnen war.
Charles Stewart
@ Charles: Haben Sie die Referenz für dieses Papier?
Rob
1
@Rob: Nein, ich habe Angst. Mir fällt ein, dass es sich möglicherweise um ein nicht beschriebenes Workshop-Papier handelte. Es gibt eine Arbeit von Danos & Joinet (2001), die einige schwache lineare Logiken, lineare Logiken und Elementarzeiten auflistet , und Sie könnten die Axiomatik daraus herausfinden: Es sollte danach gesucht werden, welche die Theoreme der Form Lp -> sind Rp, wobei L & R eine beliebige Zeichenfolge von Modaloperatoren verwendet und feststellt, mit welchen ähnlichen Sätzen der regulären Modallogik sie übereinstimmen.
Charles Stewart
@ Charles - danke! Ich werde es mir ansehen.
Rob
7

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.

Charles Stewart
quelle
6

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

rauben
quelle