Znalezienie skończonego modelu

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ń.

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.

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.

1. Logika modalna i niezmiennik bisimulacyjny fragmentu dwóch zmiennych FOL.
2. CTL * i bisimulacyjny niezmienny fragment logiki ścieżki monadycznej.
3. 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.

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:

1. 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.

2. Przypadki, w których możliwa jest eliminacja kwantyfikatora : teorii.stanford.edu/~tingz/talks/qe.ps

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