Zautomatyzowane twierdzenie dowodzące w logice liniowej

Czy automatyczne dowodzenie twierdzeń i przeszukiwanie dowodów jest łatwiejsze w liniowych i innych zdaniach logiki strukturalnej pozbawionej kurczenia?

Gdzie mogę przeczytać więcej o automatycznym dowodzeniu twierdzeń w tych logikach i roli skurczu w poszukiwaniu dowodów?

Inne zasoby można znaleźć w pracy Kaustuva Chaudhuriego „ Skoncentrowana metoda odwrotna dla logiki liniowej ”, a może zainteresować Cię „Bezkontraktowa sekwencyjna kalkulacja Roya Dyckhoffa ”, która dotyczy skurczu, ale nie logiki liniowej.

Istnieją możliwości efektywnego wyszukiwania dowodów w logice liniowej, ale nie sądzę, aby obecna praca wskazywała na to, że jest to łatwiejsze niż wyszukiwanie dowodów w logice niepodstawowej. Problemem jest to, że jeśli chcesz, aby udowodnić w logice liniowego, masz dodatkowe pytania, na które nie masz w normalnym wyszukiwaniu Dowód: Jest C wykorzystane do udowodnienia A czy jest C wykorzystane do udowodnienia B ? W praktyce ten „niedeterminizm zasobów” stanowi duży problem podczas wyszukiwania dowodów w logice liniowej.$C \vdash(A \otimes B)$$C$$A$$C$$B$

Zgodnie z komentarzami Lincoln i wsp. Z 1990 r. „ Problemy decyzyjne dla logiki liniowej zdań ” są dobrym odniesieniem, jeśli chcesz uzyskać techniczne uwagi na temat słów takich jak „łatwiej”.

Nie, jest tylko coraz trudniej.

Podobnie jak problem decyzyjny dla intuicyjnej logiki zdań jest trudniejszy niż w przypadku klasycznej logiki zdań, tak też liniowa logika zdań jest jeszcze trudniejsza. Zarówno wykładniczymi (które nie brakuje skurczu), jak i różnymi smakami nieprzemiennego połączenia, logika staje się nierozstrzygalna, a nawet słabe klasyczne MALL jest kompletne PSPACE. Dla kontrastu, problem decyzyjny dla klasycznej logiki zdań jest co-NP kompletny, a dla intuicyjnej logiki zdań, PSPACE kompletny. (Offhand, nie znam złożoności intuicyjnego MALL.)

Polecam wykład Pata Lincolna w części 6 jego Logiki liniowej , SIGACT News 1992. Od tego czasu dowiedzieliśmy się nieco więcej, to znaczy, mamy wyniki dla dużej rodziny logiki liniowej, ale podstawowy obraz jest.

W pewnym sensie to sprawia, że ​​poszukiwanie dowodu logiki liniowej jest interesujące, ponieważ twardość problemu decyzyjnego tworzy przestrzeń dla bardziej interesujących pojęć obliczeniowych, a logika liniowa jest trudna na wiele różnych sposobów. Andrej wskazał na przegląd programowania liniowego logiki Dale'a Millera ; jest to dobre miejsce, skoro Miller zrobił więcej, aby rozwinąć pomysł wyszukiwania dowodów tak samo jak obliczenia .

Zakładając, że złożoność problemu sprawdzalności byłaby dla ciebie satysfakcjonująca, krajobraz złożoności logiki podstrukturalnej z i bez skurczu jest nieco złożony. Spróbuję tutaj zbadać, co jest znane z logiki zdań i logiki zdań. Krótka odpowiedź jest taka, że ​​skurcz czasami pomaga (np. LLC jest rozstrzygalny, a LL nie), a czasami nie (np. MALL jest kompletny z PSPACE, MALLC jest kompletny z ACKERMANN).

Logika zdań

• CL: logika klasyczna
• IL: logika intuicyjna
• LL: logika liniowa, fragmenty MLL (multiplikatywny), MELL (multiplikatywny wykładniczy), MALL (multiplikatywny dodatek)
• LLW: logika afiniczna, tj. LL z osłabieniem, takie same fragmenty jak powyżej
• LLC: skurczowa logika liniowa, tj. LL ze skurczem, takie same fragmenty jak powyżej
• $_\to$$_{\to,\wedge}$

Złożoność niezawodności

• NP-complete: MLL [Kan91]
• co-NP-complete: CL
• PSPACE-complete: IL [Sta79], MALL [Lin92]
• $_\to$
• TOWER-complete: MELLW, LLW [Laz14]
• $_{\to,\wedge}$
• $\Sigma_1^0$

$_\to$

Bibliografia

• [Kan91] Max Kanovich, Multiplikatywny fragment logiki liniowej jest NP-zupełny , Raport z badań X-91-13, Instytut Języka, Logiki i Informacji, 1991.
• [Laz14] Ranko Lazić i Sylvain Schmitz, Niepodzielne złożoności dla rozgałęziania VASS, MELL i rozszerzenia , rękopis, 2014. arXiv: 1401.6785 [cs.LO]
• [Lin92] Patrick Lincoln, John Mitchell, Andre Scedrov i Natarajan Shankar, Problemy decyzyjne dla logicznej logiki zdań , Annals of Pure and Applied Logic 56 (1–3): 239–311, 1992. 10.1016 / 0168-0072 (92) 90075-B
• [Sch14] Sylvain Schmitz, Implicational Relevance Logic is 2-ExpTime-complete , manuscript, 2014. arXiv: 1402.0705 [cs.LO]
• [Sta79] Richard Statman, Intuicyjna logika zdań jest kompletna do wielomianowej przestrzeni , Theoretical Computer Science 9 (1): 67–72, 1979. doi: 10.1016 / 0304-3975 (79) 90006-9
• [Urq84] Alasdair Urquhart, Nierozstrzygalność uwikłania i stosowne implikacje , Journal of Symbolic Logic 49 (4): 1059–1073, 1984. doi: 10.2307 / 2274261
• [Urq99] Alasdair Urquhart, Złożoność procedur decyzyjnych w związku z logiką II , Journal of Symbolic Logic 64 (4): 1774–1802, 1999. 10.2307 / 2586811

Być może przegląd programowania logiki liniowej w Dale Miller jest dobrym punktem wyjścia?