Najnowocześniejszy w klasie Monadic?

11

Monadyczna logika pierwszego rzędu, znana również jako monadyczna klasa problemu decyzyjnego, jest miejscem, w którym wszystkie predykaty biorą jeden argument. Został rozstrzygnięty przez Ackermanna i jest NEXPTIME-complete .

Jednak problemy takie jak SAT i SMT mają szybkie algorytmy do ich rozwiązania, pomimo teoretycznych ograniczeń.

Zastanawiam się, czy istnieją badania analogiczne do SAT / SMT dla logiki monadycznej pierwszego rzędu? Jaki jest „stan techniki” w tym przypadku i czy istnieją algorytmy, które są skuteczne w praktyce, pomimo osiągnięcia teoretycznych limitów w najgorszym przypadku?

— jmite
źródło

3

Znalazłem oznaki, że taka procedura decyzyjna została wdrożona w twierdzeniu (ogólnym celu) SPASS .

W szczególności patrz teza Ann-Christin Knoll, dotycząca procedur decyzyjnych dotyczących fragmentu monadycznego i strzeżonego fragmentu negacji. To implementuje to, czego chcesz, ale nie mogłem znaleźć implementacji online.

— cody
źródło

2

W artykule LICS z 1993 r. Bachmair, Ganzinger i Waldmann wykazali, że ustawione ograniczenia są równoważne monadycznemu FOL, natomiast w zestawach ograniczeniowych jest klasa monadyczna . Jeśli pamięć służy, ustawione ograniczenia są równoważne zwykłym gramatykom drzewa, więc większość opracowanych tam algorytmów powinna również być przenośna na monadyczny FOL.

Nie znam tego obszaru zbyt dobrze, ale ustalone ograniczenia i zwykłe gramatyki drzew były szeroko stosowane w analizie programu, więc należy opracować dla nich praktyczne algorytmy.

— Neel Krishnaswami
źródło

Tak ... Przyznaję, że moim zainteresowaniem klasą monadyczną jest rozwiązywanie ustalonych ograniczeń, więc mamy pewien problem z kurczakiem i jajkami. Większość tego, co znalazłem dla określonych ograniczeń w analizie programu, takich jak Banshee, dotyczy klas ograniczonych, które są słabsze niż klasa monadyczna (tj. Nie mają negacji ani projekcji). Ale mogłem przegapić kilka.

— jmite