Zautomatyzowane twierdzenie dowodzące w logice liniowej

18

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?

— Anonimowy
źródło

17

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 wykorzystane do udowodnienia czy jest wykorzystane do udowodnienia ? 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”.

— Rob Simmons
źródło

3

! A

$!A$

4

@Neel: Wykładnicze są urządzeniem, które z powrotem wykracza skurcz. Ponadto łączniki addytywne zachowują się wewnętrznie tak, jakby miały skurcz, więc nie chcesz ich też. Pozostaje Ci MLL, który rzeczywiście jest NP-zupełny (w przeciwieństwie do klasycznej logiki, która nie jest NP-pełna, jak powiedziałeś, ale coNP-pełna). W szczególności każda tautologia MLL ma dowód wielkości wielomianowej. Jednak ten dowód nie jest łatwy do znalezienia deterministycznie, jak wyjaśnia Rob (co jest dobrą rzeczą, ponieważ chcemy, aby NP nie było w czasie podwykonawczym.)

— Emil Jeřábek popiera Monikę

1

Obaj słusznie zwracacie uwagę, że mówiłem bardzo nieformalnie o tym, dlaczego logika liniowa nie jest „łatwiejsza” - w sensie formalnym wyszukiwanie dowodu MALL jest trudniejsze, a pełne wyszukiwanie dowodu logicznego jest jeszcze trudniejsze. Większość, jeśli nie wszystkie, wyniki, o których będzie mowa, pochodzą od Lincolna i innych w artykule z 1990 r. „Problemy decyzyjne dla logiki logicznej zdań”.

— Rob Simmons,

1

c u t

$\it cut$

A

$A$

1

@Rob Simmons: zadowalające zadanie dla jego negacji.

— Kaveh

11

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 .

— Charles Stewart
źródło

@Kaveh: Niepoprawne wyszukiwanie zamiast literówki; naprawiony. Powinienem wspomnieć o MLL.

— Charles Stewart

11

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

— Sylvain
źródło

9

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

— Andrej Bauer
źródło