Znalezienie skończonego modelu

11

Wiem, że pytanie „czy formuła pierwszego rzędu ma model” jest ogólnie nierozstrzygalne. $\phi$

Czy ktoś mógłby mi dać link lub książkę, która da odpowiedź na skończone modele. Jeśli mam wzór pierwszego rzędu , czy można rozstrzygnąć, czy ma model skończony? Jestem pewien, że pytanie jest dobrze znane, ale nawet nie wiem od czego zacząć szukanie odpowiedzi. (Na przykład spodziewałbym się, że będzie to w „Elementach teorii modeli skończonych” Libkina, ale wydaje się, że nie mogę go znaleźć.) $\phi$ $\phi$

Druga część mojego pytania brzmi: czy są znane ograniczenia, które powodują, że problem jest rozstrzygalny?

Na przykład problem może stać się rozstrzygalny dla formuły pierwszego rzędu z tylko predykatami monadycznymi. Lub gdy mamy predykat monadyczny plus relację następcy. Ale nie wyobrażam sobie algorytmu, który decydowałby, czy istnieje (skończony) model w stosunku do tych ograniczeń.

— Arthur MILCHIOR
źródło

Czy czytałeś jakieś książki na temat teorii modeli skończonych?

— Dave Clarke

@Dave Clarke: Książka Libkina „Element teorii modeli skończonych” i „Złożoność opisowa” Immermana

— Arthur MILCHIOR

Czy szukasz twierdzenia Trakhtenbrota? W drugiej części jednym prostym przykładem jest to, że MSO nad słowami, oznaczające zwykłe języki, można sprawdzić pod kątem satysfakcji, ponieważ sama struktura słów jest czymś, co można opisać w MSO.

— Michaël Cadilhac,

Merci Michaël. Wygląda na to, że rzeczywiście odpowiada na pierwszą część mojego pytania. Ale wciąż szukam tego, co wiadomo o ograniczeniach.

— Arthur MILCHIOR

1

@ Michaël Cadilhac - Dlaczego nie opublikować odpowiedzi? Twierdzenie Trakhtenbrota jest omówione w książce Libkina w rozdziale 9.

— Marc Hamann

14

Na pierwszą część twojego pytania odpowiada twierdzenie Trakhtenbrota . Druga część jest rzeczywiście dość dużym pytaniem. W zależności od struktury relacyjnej, nad którą pracujesz, możesz podać wiele rozwiązań. Na przykład, jeśli interesują Cię języki formalne, MSO nad strukturami słów odpowiada zwykłym językom, a logika dopasowywania ( zobacz to ) odpowiada CFL, a zatem ich problem z zadowalalnością jest rozstrzygalny.

Powinieneś rzucić okiem na rozdział 14 Libkina, w którym udowodniono, że ładne segmenty FO mają rozstrzygający problem z zadowalalnością, zgodnie z dopuszczalną liczbą alternatywnych kwantyfikatorów.

— Michaël Cadilhac
źródło

2

Jak mówi Michaël, duża część logiki obliczeniowej wydaje się poświęcona znajdowaniu i badaniu fragmentów, w których związane z nimi problemy są rozstrzygalne (lub możliwe do rozwiązania). Wystarczy wspomnieć o jednej miłej ankiecie: Gottlob, Kolaitis, Schwentick, Egzystencjalna logika drugiego rzędu nad grafami: Wyznaczanie granicy podatności , JACM 2004, dx.doi.org/10.1145/972639.972646

— András Salamon

Dziękuję za Twoją odpowiedź. W przypadku pytania, o którym myślałem, wiadomo, że jest ono równe MSO, ale obejmuje zagnieżdżone słowa. Stąd, jeśli dowód rozstrzygalności MSO nad słowami użyje dowodu rozstrzygalności niedomówień CFL, to tak naprawdę mi nie pomaga. I dzięki za „pasującą logikę”, nie wiedziałem o tym, ale wygląda bardzo podobnie do zagnieżdżonych słów, dlatego może mnie zainteresować.

— Arthur MILCHIOR

4

Nie znam odpowiedzi na arbitralne fragmenty FO. Klasyczna logika modalna i jej rozszerzenia mają kilka właściwości rozstrzygalności. Dzięki standardowym tłumaczeniom otrzymujesz fragmenty klasycznej logiki, które mają te same właściwości.

Logika modalna i niezmiennik bisimulacyjny fragmentu dwóch zmiennych FOL.
CTL * i bisimulacyjny niezmienny fragment logiki ścieżki monadycznej.
Rachunek mu i bisimulacyjny niezmienny fragment logiki Monadic drugiego rzędu.

Wszystkie powyższe logiki modalne są rozstrzygalne i mają właściwość modelu skończonego. Inne logiki o solidnych właściwościach rozstrzygalności to strzeżony fragment FO, luźno strzeżony fragment i strzeżona logika stałego punktu. Te logiki zostały zaprojektowane w celu przeniesienia istoty dobrze zachowanych właściwości logiki modalnej do klasycznego układu logicznego. Chroniona logika punktu stałego jest rozstrzygalna, ale nie ma właściwości modelu skończonego.

— Vijay D.
źródło

1

To, co następuje, nie powinno być traktowane jako żadna prawda z podręcznika magisterskiego, a jedynie sugestie do dalszych badań. Redaktorzy mogą wprowadzać poprawki według własnego uznania.

Po pierwsze, twoje pytanie jest najwyraźniej interesujące dla społeczności Automated Deduction. William McCune ma program o nazwie Mace4, który wyszukuje modele skończone. Możesz przeczytać dokumentację opisującą, jak to zrobić.

Jeśli chodzi o konkretne ograniczenia rozstrzygalne, możesz spojrzeć na następujące kwestie:

Przypadki, w których wszechświat Herbrand jest skończony. Jednym z mechanicznych sposobów sprawdzania podzbioru tych przypadków jest sprawdzenie, czy formuła ma jakieś symbole funkcji. Jeśli nie, wszechświat Herbrand jest skończony.
Przypadki, w których możliwa jest eliminacja kwantyfikatora : teorii.stanford.edu/~tingz/talks/qe.ps

— Nieśmiała osoba
źródło

0

Oprócz udzielonych już odpowiedzi: bardzo dobrym odniesieniem do (nie) rozstrzygalności fragmentów logiki pierwszego rzędu jest książka Klasyczny problem decyzyjny autorstwa Börgera, Grädela i Gurevicha

— fh
źródło