Ein endliches Modell finden

11

$\phi$

$\phi$ $\phi$

Der zweite Teil meiner Frage lautet: Gibt es bekannte Einschränkungen, so dass das Problem entscheidbar ist?

Beispielsweise kann das Problem für Formeln erster Ordnung mit nur monadischen Prädikaten entscheidbar werden. Oder wenn wir ein monadisches Prädikat plus eine Nachfolgerbeziehung haben. Aber ich kann mir keinen Algorithmus vorstellen, um zu entscheiden, ob es ein (endliches) Modell für diese Einschränkungen gibt.

reference-request lo.logic computability finite-model-theory Arthur MILCHIOR
quelle

Haben Sie Bücher über endliche Modelltheorie gelesen?

Dave Clarke

@ Dave Clarke: Libkins Buch "Element of Finite Model Theory" und Immermans "Descriptive Complexity"

Arthur MILCHIOR

Suchen Sie nach dem Satz von Trakhtenbrot? Für den zweiten Teil ist ein einfaches Beispiel, dass MSO über Wörtern, die reguläre Sprachen bezeichnen, auf Erfüllbarkeit überprüft werden kann, da die Wortstruktur selbst etwas ist, das man in MSO beschreiben kann.

Michaël Cadilhac

Merci Michaël. Es scheint tatsächlich den ersten Teil meiner Frage zu beantworten. Aber ich suche immer noch, was über Einschränkungen bekannt ist.

Arthur MILCHIOR

1

@ Michaël Cadilhac - Warum nicht eine Antwort posten? Der Satz von Trakhtenbrot wird in Libkins Buch in Kapitel 9 behandelt.

Marc Hamann

14

Der erste Teil Ihrer Frage wird durch den Satz von Trakhtenbrot beantwortet . Der zweite Teil ist in der Tat eine ziemlich große Frage. Abhängig von der relationalen Struktur, an der Sie arbeiten, können mehrere Lösungen angegeben werden. Wenn Sie beispielsweise an formalen Sprachen interessiert sind, entspricht MSO über Wortstrukturen regulären Sprachen, und die Übereinstimmungslogik ( siehe dies ) entspricht CFL, sodass das Problem der Erfüllbarkeit entscheidbar ist.

Sie sollten sich Kapitel 14 von Libkin ansehen, in dem nachweislich schöne FO-Segmente je nach Anzahl der zulässigen Quantifiziererwechsel ein entscheidbares Erfüllbarkeitsproblem aufweisen.

Michaël Cadilhac
quelle

2

Wie Michaël sagt, scheint ein großer Teil der Rechenlogik darauf ausgerichtet zu sein, Fragmente zu finden und zu untersuchen, bei denen die damit verbundenen Probleme entscheidbar (oder nachvollziehbar) sind. Um nur eine schöne Umfrage zu erwähnen: Gottlob, Kolaitis, Schwentick, Existenzielle Logik zweiter Ordnung über Graphen: Darstellung der Traktabilitätsgrenze, JACM 2004, dx.doi.org/10.1145/972639.972646

András Salamon

Vielen Dank für Ihre Antwort. Für die Frage, über die ich nachgedacht habe, ist bekannt, dass sie MSO entspricht, jedoch über verschachtelte Wörter. Wenn also der Beweis der Entscheidbarkeit von MSO über Wörter den Beweis der Entscheidbarkeit der Leere von CFL verwendet, hilft es mir nicht wirklich. Und danke für die "Matching-Logik", die ich nicht kannte, aber sie sieht sehr nach verschachtelten Wörtern aus und könnte mich daher interessieren.

Arthur MILCHIOR

4

Ich kenne die Antwort für beliebige FO-Fragmente nicht. Die klassische Modallogik und ihre Erweiterungen haben mehrere Entscheidbarkeitseigenschaften. Bei den Standardübersetzungen erhalten Sie Fragmente der klassischen Logik, die diese Eigenschaften gemeinsam haben.

Modal Logic und das bisimulationsinvariante Fragment von FOL mit zwei Variablen.
CTL * und das bisimulationsinvariante Fragment der monadischen Pfadlogik.
Der Mu-Kalkül und das bisimulationsinvariante Fragment der monadischen Logik zweiter Ordnung.

Alle oben genannten Modallogiken sind entscheidbar und haben die Eigenschaft des endlichen Modells. Andere Logiken mit robusten Entscheidbarkeitseigenschaften sind das geschützte Fragment von FO, das lose geschützte Fragment und geschützte Fixpunktlogiken. Diese Logiken wurden entwickelt, um die Essenz gut erzogener Eigenschaften modaler Logiken auf eine klassische Logikeinstellung zu übertragen. Die geschützte Festpunktlogik ist entscheidbar, verfügt jedoch nicht über die Eigenschaft des endlichen Modells.

Vijay D.
quelle

1

Was folgt, sollte nicht als Lehrbuchwahrheit verstanden werden, sondern lediglich als Vorschlag für Ihre eigene weitere Forschung. Redakteure können nach eigenem Ermessen Korrekturen vornehmen.

Erstens ist Ihre Frage anscheinend für die Automated Deduction-Community von Interesse. William McCune hat ein Programm namens Mace4, das nach endlichen Modellen sucht. Vielleicht möchten Sie die Dokumentation lesen, in der beschrieben wird, wie es gemacht wird.

In Bezug auf bestimmte entscheidbare Einschränkungen sollten Sie Folgendes beachten:

Fälle, in denen das Herbrand-Universum endlich ist. Eine mechanische Methode zum Überprüfen einer Teilmenge dieser Fälle besteht darin, zu überprüfen, ob die Formel Funktionssymbole enthält. Wenn nicht, ist das Herbrand-Universum endlich.
Fälle, in denen die Eliminierung von Quantifizierern möglich ist: Theory.stanford.edu/~tingz/talks/qe.ps

Schüchterne Person
quelle

0

Neben den bereits gegebenen Antworten: Eine sehr gute Referenz zur (Un-) Entscheidbarkeit von Fragmenten der Logik erster Ordnung ist das Buch Das klassische Entscheidungsproblem von Börger, Grädel und Gurevich

fh
quelle