Recherche d'articles et d'articles sur les logiques sous-structurales modales

15

Je recherche des articles et des articles sur les logiques modales sous-structurelles - non pas sur la sémantique des modalités de logique linéaire, mais sur les logiques sous-structurelles augmentées d'opérateurs modaux standard, par exemple sous-structuraux K (quelque chose comme MALL avec opérateur de boîte, nécessité et règles K).

Rob
la source

Réponses:

13

Je connais des travaux ajoutant des modalités temporelles à la logique linéaire pour produire ce qu'on a appelé la logique linéaire temporelle (contrairement à LTL = logique temporelle linéaire-temps). C'est assez intéressant: une formule (sans modalité) est interprétée comme des ressources disponibles maintenant . La prochaine modalité temporelle est interprétée comme des ressources disponibles au pas de temps suivant. La modalité de boîte - signifie que les ressources peuvent être consommées à tout moment dans le futur, déterminé par le détenteur des ressources , alors que - signifie que les ressources peuvent être consommées à tout moment déterminé par le système---. Remarquez la dualité entre le détenteur de la ressource et le système.

Il existe quelques articles ajoutant toutes sortes de modalités à la logique linéaire et affine:

Les travaux sur la logique linéaire temporelle ont été appliqués à la programmation et à la coordination orientées agents, faisant un usage essentiel de l'interprétation des modalités décrites ci-dessus:

Dave Clarke
la source
8

Ce type de logiques est considéré en linguistique: vous pouvez consulter l'article de Michael Moortgat, Categorial Type Logic .

Noam Zeilberger
la source
8

Une modalité de logique linéaire est un opérateur de boîte satisfaisant les axiomes S4.

Il est bien connu que l'unicité de! A n'est pas dérivable - c'est-à-dire que si vous avez un bang rouge et un bang bleu, qui satisfont tous deux séparément aux règles du bang, vous ne pouvez pas prouver qu'ils sont équivalents. Je ne me souviens pas par hasard où ce résultat peut être trouvé, mais c'est probablement dans l'article de Girard de 1987 sur la logique linéaire.

EDIT: J'ai demandé à Jason Reed, dont la thèse portait sur les encodages de la logique linéaire en logique hybride, et il m'a pointé vers l'article suivant de Chaudhuri et Despeyroux, "A Logic for Constrained Process Calculi with Applications to Molecular Biology" . Ils étendent la logique linéaire intuitionniste avec des annotations hybrides destinées à refléter la logique temporelle, et ils en ont fait un travail très propre - ils prouvent non seulement la suppression des coupures, mais aussi la focalisation. Il semble donc qu'il devrait être simple de simplifier leur calcul pour obtenir le modal K à la Simpson.

Neel Krishnaswami
la source
1
Je cherche quelque chose de plus faible, qui correspond à K plutôt qu'à S4.
Rob
1
@Rob: quelques modalités plus faibles pour la logique linéaire sont étudiées en logique linéaire légère. J'ai vu un document décrivant la relation entre trois LLL et les logiques modales Kripkean standard, mais j'oublie laquelle et si K en faisait partie.
Charles Stewart
@Charles: avez-vous la référence pour cet article?
Rob
1
@Rob: Non, j'ai peur. Il me semble que ce pourrait être un document d'atelier qui n'a pas été rédigé. Il y a un article de Danos et Joinet (2001) qui énumère quelques logiques linéaires faibles, la logique linéaire et le temps élémentaire , et vous pourriez en comprendre les axiomatiques: il devrait suivre en regardant quels sont les théorèmes de la forme Lp -> Rp, où L&R n'importe quelle chaîne d'opérateurs modaux, et voir quels théorèmes similaires de logique modale régulière ils correspondent.
Charles Stewart
@Charles - merci! Je vais y jeter un œil.
Rob
7

Actuellement, la théorie de la preuve la plus systématique qui permet à de nombreuses logiques modales d'être superposées à de nombreuses logiques sous-structurelles est la logique d'affichage de Belnap, qui a reçu un traitement décent de la part de Marcus Kracht - voir en particulier sa puissance et sa faiblesse de la logique d'affichage modale , 1996 - et Heinrich Wansing, Displaying Modal Logic , 1998.

La logique d'affichage a des problèmes pour gérer la logique non commutative, qui était l'une des motivations derrière quelques thèses de maîtrise que j'ai supervisées il y a quelques années, pour appliquer quelques idées sur la représentation des modalités dans le calcul des structures, qui est très puissant pour représenter les logiques sous-structurelles, mais a couru en raison de la façon inhabituelle dont l'élimination des coupures est prouvée dans ce Les travaux de Robert Hein sur la génération de règles pour les logiques modales à partir de familles d'axiomes, résumés dans Pureté par le démêlage, 2005, couvre la plupart des logiques habituelles (les axiomes les plus importants non couverts sont B, CR et L), et il existe des preuves circonstancielles assez solides pour croire la conjecture d'élimination des coupures. Aucun de ces travaux ne traite réellement de la logique sous-structurelle, mais si un type plus fort de théorème d'élimination des coupures était prouvé pour ces modalités, le soi-disant lemme de fractionnement, cela rendrait la logique très modulaire et l'élimination des coupures devrait suivre facilement pour toutes les manières de coller les logiques.

La logique sous-structurelle n'a pas vraiment une notion uniforme de sémantique, mais pour la logique sous-structurale modale, nous avons une sorte de recette pour transformer la sémantique de la logique de base en sémantique de logiques modales correspondantes, en étendant une sémantique de type trace avec une notion de cadre ou une sémantique algébrique / catégorique avec une notion d'opérateur. Kracht et Wansing travaillent dans ces deux directions.

Charles Stewart
la source
6

J'ai parcouru Norihiro Kamide, "Kripke Semantics for Modal Substructural Logics", Journal of Logic, Language and Information 11 (4) , 2002, ce qui n'est pas tout à fait ce que je voulais, mais les références citent Marcello D'Agostino et Dov M. Gabbay et Alessandra Russo, "Modalités de greffe sur les systèmes d'implication sous-structurels", Studia Logica 59 , 1996, ce qui semble être ce que je recherche. C'est sur CiteSeer http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.5719

Rob
la source