Dobre referencje na temat przybliżonych metod rozwiązywania problemów logicznych

Wiadomo, że wiele problemów logicznych (np. Problemy satysfakcji kilku logik modalnych) nie są rozstrzygalne. Istnieje również wiele nierozstrzygalnych problemów w teorii algorytmów, np. W optymalizacji kombinatorycznej. Ale w praktyce heurystyki i algorytmy przybliżone działają dobrze w przypadku algorytmów praktycznych.

Można więc oczekiwać, że odpowiednie będą również algorytmy przybliżone dla problemów logicznych. Jednak jedynym trendem w tym zakresie, jaki udało mi się znaleźć, jest problem maksymalnej liczby satelitów, a jego rozwój był aktywny w latach dziewięćdziesiątych.

Czy są jakieś inne aktywne trendy badawcze, warsztaty, słowa kluczowe, dobre referencje do stosowania i rozwoju przybliżonych metod logiki modalnej, programowania logiki i tak dalej?

Jeśli oczekuje się, że zautomatyzowane rozumowanie zyska na znaczeniu w przyszłych zastosowaniach informatyki, wówczas trzeba będzie wyjść poza ograniczenia nierozstrzygalności wynikające z logiki, a przybliżone metody lub heurystyka mogą być naturalną ścieżką, prawda?

Motywacja, którą podajesz za radzenie sobie z nierozstrzygalnością, dotyczy również rozstrzygalnych, ale trudnych problemów. Jeśli masz problem, który jest trudny do NP lub PSPACE, zazwyczaj będziemy musieli zastosować jakieś przybliżenie (w szerokim znaczeniu tego słowa), aby znaleźć rozwiązanie.

Przydatne jest rozróżnianie różnych pojęć przybliżenia.

• $\varepsilon$
• $\delta$

$(\varepsilon,\delta)$

Oto przykład innego pojęcia przybliżenia. Załóżmy, że wykonujesz obliczenia, takie jak pomnożenie dwóch dużych liczb, i chcesz sprawdzić, czy mnożenie było prawidłowe. Istnieje wiele technik heurystycznych, które są stosowane w praktyce do sprawdzania poprawności bez powtarzania obliczeń. Możesz sprawdzić, czy znaki zostały pomnożone, aby uzyskać odpowiedni znak. Możesz sprawdzić, czy liczby mają odpowiednią parzystość (właściwości liczb parzystych / nieparzystych). Możesz użyć bardziej zaawansowanego czeku, takiego jak Rzucanie dziewiątek. Wszystkie te techniki mają wspólną właściwość, którą mogą powiedzieć, jeśli popełniłeś błąd, ale nie mogą zagwarantować, że uzyskasz właściwą odpowiedź. Ta właściwość może być postrzegana jako logiczne przybliżenie, ponieważ możesz być w stanie udowodnić, że oryginalne obliczenie jest nieprawidłowe, ale możesz nie być w stanie udowodnić, że jest poprawne.

Wszystkie kontrole, o których wspomniałem powyżej, są przykładami techniki zwanej interpretacją abstrakcyjną. Interpretacja abstrakcyjna czyni całkowicie rygorystycznym pojęcie logicznego przybliżenia odrębne od przybliżeń numerycznych i probabilistycznych. Problem, który opisałem przy analizie pojedynczego obliczenia, obejmuje bardziej złożony przypadek analizy programu. W literaturze dotyczącej interpretacji abstrakcyjnej opracowano techniki i ramy przybliżonego, logicznego rozumowania programów, a ostatnio także logiki. Przydatne mogą być następujące odniesienia.

1. Streszczenie Interpretacja w pigułce autorstwa Patricka Cousota, która jest prostym przeglądem.
2. Omówienie abstrakcji Patricka Cousota w ramach jego kursu. Istnieje bardzo ładny przykład abstrakcji do określania właściwości kufla kwiatów. Analogia bukietu zawiera punkty stałe i może być wykonana całkowicie matematycznie.
3. Kurs abstrakcyjnej interpretacji autorstwa Patricka Cousota, jeśli chcesz uzyskać głębię i szczegóły.
4. Abstrakcyjna interpretacja i zastosowanie do programów logicznych , Patrick Cousot i Radhia Cousot, 1992. Dotyczy programów logicznych, zgodnie z twoją prośbą. Część początkowa formalizuje również procedurę wyrzucania dziewiątek jako interpretację abstrakcyjną.

Wszystko to zwykle stosuje się do rozumowania programów komputerowych. Niedawno przeprowadzono prace nad zastosowaniem pomysłów z interpretacji abstrakcyjnej do badania procedur decyzyjnych w zakresie logiki. Nie skupiono się na logice modalnej, ale na satysfakcji w logice zdań i teoriach pierwszego rzędu wolnych od kwantyfikatorów. (Ponieważ pracowałem w tej przestrzeni, jeden papier poniżej jest mój)

1. Uogólnienie metody Staalmarcka autorstwa Adityi Thakur i Thomasa Repsa, 2012. Uogólnia metodę Staalmarcka na problemy w analizie programu.
2. Zredukowany produkt domen abstrakcyjnych i połączenie procedur decyzyjnych , Patrick Cousot, Radhia Cousot i Laurent Mauborgne, 2011. W tym dokumencie badano technikę Nelsona-Oppena do łączenia procedur decyzyjnych i pokazano, że można go również stosować do niekompletnych kombinacji, które jest szczególnie interesujący, jeśli masz nierozwiązywalne problemy.
3. Solvery satysfakcji to Static Analyzers , moja praca z Leopoldem Hallerem i Danielem Kroeningiem, 2012. Stosuje widok przybliżenia oparty na sieci, aby scharakteryzować istniejące solvery. Zamiast tego możesz także spojrzeć na moje slajdy na ten temat .

Teraz żaden z powyższych artykułów nie odpowiada na konkretne pytanie dotyczące atakowania problemów satysfakcji, których nie można rozstrzygnąć. Dokumenty te mają podejście logiczne zorientowane na przybliżenie, które nie ma charakteru numerycznego ani probabilistycznego. Ten pogląd został szeroko zastosowany do rozumowania programów i uważam, że dotyczy dokładnie tego, o co prosisz.

Aby zastosować go do logiki modalnej, sugerowałbym, aby rozpocząć od semantyki algebraicznej Jonssona i Tarskiego lub późniejszej semantyki Lemmona i Scotta. Wynika to z faktu, że abstrakcyjna interpretacja formułowana jest w kategoriach sieci i funkcji monotonicznych, więc algebry logiczne z operatorami są wygodną semantyką do pracy. Jeśli chcesz zacząć od ramek Kripkego, możesz zastosować twierdzenie o dualności Jonssona i Tarskiego (które niektórzy mogą nazwać dualnością kamienną) i uzyskać algebraiczną reprezentację. Następnie można zastosować twierdzenia o abstrakcyjnej interpretacji dla logicznego przybliżenia.