À procura de artigos e artigos sobre lógicas subestruturais modais

15

Eu estou procurando artigos e artigos sobre lógicas estruturais subestruturais - não sobre a semântica de modalidades lógicas lineares, mas sobre lógicas subestruturais aumentadas com operadores modais padrão, por exemplo, K estrutural (algo como MALL com operador de caixa, necessidade e regras K).

Roubar
fonte

Respostas:

13

Conheço o trabalho de adicionar modalidades temporais à lógica linear para produzir o que foi chamado de lógica linear temporal (em contraste com LTL = lógica temporal linear-tempo). Isso é bastante interessante: uma fórmula (sem uma modalidade) é interpretada como recursos disponíveis agora . A próxima vez que a modalidade for interpretada como recursos disponíveis na próxima etapa. A modalidade box - significa que os recursos podem ser consumidos em qualquer ponto no futuro, determinado pelo detentor dos recursos , enquanto - significa que os recursos podem ser consumidos em qualquer momento no tempo determinado pelo sistema---. Observe a dualidade entre o detentor do recurso e o sistema.

Existem alguns artigos que adicionam todos os tipos de modalidades à lógica linear e afim:

O trabalho sobre lógica linear temporal foi aplicado na programação e coordenação orientada a agentes, fazendo uso essencial da interpretação das modalidades descritas acima:

Dave Clarke
fonte
8

Esse tipo de lógica é considerado na linguística: você pode dar uma olhada no artigo de Michael Moortgat, Categorial Type Logic .

Noam Zeilberger
fonte
8

A! Uma modalidade de lógica linear é um operador de caixa que satisfaz os axiomas S4.

É sabido que a singularidade de! A não é derivável - ou seja, se você tem um estrondo vermelho e um estrondo azul, os quais satisfazem separadamente as regras do estrondo, não é possível provar que são equivalentes. Não me lembro de imediato onde esse resultado pode ser encontrado, mas provavelmente está no artigo de Girard, de 1987, sobre lógica linear.

Edição: Perguntei a Jason Reed, cuja tese era sobre codificações da lógica linear na lógica híbrida, e ele me indicou o seguinte artigo de Chaudhuri e Despeyroux, "Uma lógica para cálculos de processos restritos com aplicações na biologia molecular" . Eles estendem a lógica linear intuicionista com anotações híbridas destinadas a espelhar a lógica temporal e fizeram um trabalho muito claro - eles provam não apenas a eliminação de cortes, mas também a focalização. Portanto, parece que deve ser simples simplificar seu cálculo para obter o modal K à la Simpson.

Neel Krishnaswami
fonte
11
Estou procurando por algo mais fraco, que corresponda a K ao invés de S4.
Rob
11
@ Rob: algumas modalidades mais fracas da lógica linear são estudadas na lógica linear leve. Vi um artigo descrevendo a relação entre três LLLs e lógicas modais kripkeanas padrão, mas esqueço quais e se K estava entre elas.
22811 Charles Stewart
@ Charles: você tem a referência para esse artigo?
Rob
11
@ Rob: Não, eu tenho medo. Ocorre-me que poderia ter sido um documento de oficina que não foi escrito. Há um artigo de Danos & Joinet (2001) que lista algumas lógicas lineares fracas, Linear Logic & Elementary Time , e você pode descobrir os axiomatics a partir disso: deve seguir procurando ver quais são os teoremas da forma Lp -> Rp, onde L&R qualquer cadeia de operadores modais e ver quais teoremas semelhantes da lógica modal regular eles correspondem.
Charles Stewart
@ Charles - obrigado! Vou dar uma olhada nisso.
6111 Rob
7

Atualmente, a teoria de prova mais sistemática que permite que muitas lógicas modais sejam aplicadas a muitas lógicas subestruturais é a lógica de exibição de Belnap, que recebeu um tratamento decente nas mãos de Marcus Kracht - veja em particular seu poder e fraqueza da lógica de exibição modal , 1996 - e Heinrich Wansing, Exibindo Modal Logic , 1998.

A lógica de exibição apresenta problemas ao lidar com lógica não comutativa, que foi uma das motivações por trás de algumas teses de mestrado que eu supervisionei há alguns anos, para aplicar algumas idéias sobre a representação de modalidades no Cálculo de Estruturas, que é muito poderoso para representar lógicas subestruturais, mas executou problemas devido à maneira incomum de eliminação de cortes é comprovada nesse cenário. O trabalho de Robert Hein sobre a geração de regras para lógicas modais a partir de famílias de axiomas, resumido em Purity Through Unraveling, 2005, abrange a maioria das lógicas usuais (os axiomas mais importantes não cobertos são B, CR e L), e há evidências circunstanciais bastante fortes para acreditar na conjectura de eliminação de cortes. Na verdade, nenhum desses trabalhos trata a lógica subestrutural, mas se um tipo mais forte de teorema de eliminação de cortes for comprovado para essas modalidades, o chamado lema de divisão, isso tornaria a lógica muito modular e a eliminação de cortes deve seguir facilmente para todas as formas de colando as lógicas.

A lógica subestrutural não tem realmente uma noção uniforme de semântica, mas, para a lógica subestrutural modal, temos um tipo de receita para transformar a semântica da lógica base em semântica de lógica modal correspondente, estendendo uma semântica semelhante a traço com uma noção de quadro ou uma semântica algébrica / categórica com uma noção de operador. Kracht e Wansing trabalham em ambas as direções.

Charles Stewart
fonte
6

Venho examinando Norihiro Kamide, "Kripke Semântica para Modal Substructural Logics", Journal of Logic, Language and Information 11 (4) , 2002, que não é exatamente o que eu queria, mas as referências citam Marcello D'Agostino e Dov M. Gabbay e Alessandra Russo, "Enxertando Modalidades em Sistemas de Implicação Subestruturais", Studia Logica 59 , 1996, que parece ser o que estou procurando. Está no CiteSeer http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.5719

Roubar
fonte