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?

reference-request lo.logic automated-theorem-proving program-verification first-order-logic jmite
źródło

Odpowiedzi:

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