Prova de teorema automatizado em lógica linear

O teorema automático de prova e pesquisa de provas é mais fácil em lógicas subestruturais lineares e outras proposicionais que carecem de contração?

Onde posso ler mais sobre o teorema automático de prova nessas lógicas e o papel da contração na pesquisa de provas?

Outros recursos podem ser encontrados na tese de Kaustuv Chaudhuri, " O método inverso focado para a lógica linear ", e você pode estar interessado no "Cálculo de sequência livre de contração " de Roy Dyckhoff , que trata de contração, mas não de lógica linear.

Existem oportunidades para a pesquisa de provas eficiente em lógica linear, mas não acho que o trabalho atual indique que seja mais fácil do que a pesquisa de provas em lógica não-estrutural. O problema é que, se você deseja provar na lógica linear, tem uma pergunta extra que não possui na pesquisa de provas normal: C é usado para provar A ou C é usado para provar B ? Na prática, esse "não determinismo de recurso" é um grande problema na realização de pesquisa de prova na lógica linear.$C \vdash(A \otimes B)$$C$$A$$C$$B$

Pelos comentários, " Problemas de decisão para a lógica linear proposicional " , de Lincoln et al., Em 1990, é uma boa referência se você deseja obter informações técnicas sobre palavras como "mais fácil".

Não, é apenas cada vez mais difícil.

Assim como o problema de decisão para a lógica proposicional intuicionista é mais difícil do que a lógica proposicional clássica, também é mais difícil a lógica proposicional linear. Com exponenciais (que não carecem de contração) ou vários sabores de conectivo não comutativo, a lógica se torna indecidível e até o fraco e clássico MALL é o PSPACE completo. Por outro lado, o problema de decisão da lógica proposicional clássica é co-NP completo e, para a lógica proposicional intuicionista, PSPACE completo. (De imediato, não conheço a complexidade do MALL intuicionista.)

Eu recomendo a exposição de Pat Lincoln na seção 6 de sua lógica linear , SIGACT News 1992. Aprendemos um pouco mais desde então, ou seja, temos resultados para uma grande família de lógicas lineares, mas a imagem básica está lá.

De certa forma, é isso que torna a pesquisa de provas pela lógica linear interessante, uma vez que a dureza do problema de decisão abre espaço para noções mais interessantes de computação, e a lógica linear é difícil de muitas maneiras diferentes. Andrej apontou para Uma visão geral da programação de lógica linear de Dale Miller ; este é um bom lugar para se procurar, já que Miller fez mais para desenvolver a idéia da pesquisa de provas tão computacional quanto qualquer outra pessoa.

Supondo que a complexidade do problema de provabilidade o satisfaça, o cenário das complexidades das lógicas subestruturais com e sem contração é algo complexo. Tentarei pesquisar aqui o que é conhecido por lógica linear proposicional e lógica proposicional. A resposta curta é que a contração às vezes ajuda (por exemplo, LLC é decidível, enquanto LL não é) e às vezes não (por exemplo, MALL é completo com PSPACE, MALLC é completo com ACKERMANN).

Lógica Proposicional

• CL: lógica clássica
• IL: lógica intuicionista
• LL: lógica linear, fragmentos MLL (multiplicativo), MELL (exponencial multiplicativo), MALL (aditivo multiplicativo)
• LLW: lógica afina, ou seja, LL com enfraquecimento, os mesmos fragmentos acima
• LLC: lógica linear contrativa, ou seja, LL com contração, os mesmos fragmentos acima
• $_\to$$_{\to,\wedge}$

Complexidade da disponibilidade

• NP completo: MLL [Kan91]
• co-NP-completo: CL
• PSPACE-complete: IL [Sta79], MALL [Lin92]
• 2EXP-completo: R$_\to$
• TORRE-concluída: MELLW, LLW [Laz14]
• $_{\to,\wedge}$ [Urq99], MALLC, LLC [Laz14]
• $\Sigma_1^0$ -completo: LL [Lin92], R [Urq84]

Algumas das principais questões em aberto aqui são se MELL é decidível e qual é a complexidade do fragmento implicacional T$_\to$

Referências

• [Kan91] Max Kanovich, O fragmento multiplicativo da lógica linear está NP-completo , Relatório de Pesquisa X-91-13, Instituto de Linguagem, Lógica e Informação, 1991.
• [Laz14] Ranko Lazić e Sylvain Schmitz, Complexidades não elementares para ramificação VASS, MELL e Extensions , manuscrito, 2014. arXiv: 1401.6785 [cs.LO]
• [Lin92] Patrick Lincoln, John Mitchell, Andre Scedrov e Natarajan Shankar, Problemas de decisão para lógica linear proposicional , Anais da lógica pura e aplicada 56 (1–3): 239–311, 1992. 10.1016 / 0168-0072 (92) 90075-B
• [Sch14] Sylvain Schmitz, Implicational Relevance Logic, está completo em 2-ExpTime , manuscrito, 2014. arXiv: 1402.0705 [cs.LO]
• [STA79] Richard Statman, a lógica proposicional intuicionista é um espaço polinomial completo , Ciência da computação teórica 9 (1): 67–72, 1979. doi: 10.1016 / 0304-3975 (79) 90006-9
• [Urq84] Alasdair Urquhart, a indecidibilidade do envolvimento e implicações relevantes , Journal of Symbolic Logic 49 (4): 1059-1073, 1984. doi: 10.2307 / 2274261
• [Urq99] Alasdair Urquhart, A complexidade dos procedimentos de decisão na Relevance Logic II , Journal of Symbolic Logic 64 (4): 1774–1802, 1999. 10.2307 / 2586811

Talvez a visão geral da programação da lógica linear de Dale Miller seja um bom ponto de partida?