Erfüllbarkeit erster Ordnung ohne endliche Modelle

Wir wissen aus dem Satz der Kirche, dass die Bestimmung der Erfüllbarkeit erster Ordnung im Allgemeinen nicht zu entscheiden ist, aber es gibt verschiedene Techniken, mit denen wir die Erfüllbarkeit erster Ordnung bestimmen können. Am naheliegendsten ist die Suche nach einem endlichen Modell. Es gibt jedoch eine Reihe von Aussagen in der Logik erster Ordnung, von denen wir zeigen können, dass sie keine endlichen Modelle haben. Zum Beispiel ist jeder Bereich, in dem eine injektive und eine nicht-surjektive Funktion arbeitet, unendlich.

Wie zeigen wir die Erfüllbarkeit von Aussagen erster Ordnung, bei denen es keine endlichen Modelle gibt oder die Existenz endlicher Modelle unbekannt ist? Beim automatisierten Beweis des Theorems können wir die Erfüllbarkeit auf verschiedene Arten bestimmen:

1. Wir können den Satz negieren und nach einem Widerspruch suchen. Wird eine gefunden, beweisen wir die Gültigkeit der Aussage erster Ordnung und damit die Erfüllbarkeit.
2. Wir verwenden Sättigung mit Auflösung und haben keine Schlussfolgerungen mehr. Meistens müssen wir unendlich viele Schlussfolgerungen ziehen, daher ist dies nicht zuverlässig.
3. Wir können Forcen verwenden, das die Existenz eines Modells und auch die Konsistenz der Theorie voraussetzt.

Ich kenne niemanden, der Forcen als mechanisierte Technik für die Prüfung automatisierter Theoreme implementiert, und es sieht nicht einfach aus, aber ich bin interessiert, ob es getan oder versucht wurde, da es verwendet wurde, um die Unabhängigkeit für eine Reihe von Aussagen zu beweisen in der Mengenlehre, die selbst keine endlichen Modelle hat.

Gibt es andere bekannte Techniken für die Suche nach Erfüllbarkeit erster Ordnung, die für das automatisierte Denken anwendbar sind, oder hat jemand an einem automatisierten Forcierungsalgorithmus gearbeitet?

Hier ist ein amüsanter Ansatz von Brock-Nannestad und Schürmann:

Wahrhaftige monadische Abstraktionen

Die Idee ist, zu versuchen, Sätze erster Ordnung in monadische Logik erster Ordnung zu übersetzen , indem einige der Argumente "vergessen" werden. Sicher ist die Übersetzung nicht vollständig : Es gibt einige konsistente Sätze, die nach der Übersetzung inkonsistent werden.

$\overline F$$F$

kann durch ein Entscheidungsverfahren überprüft werden und impliziert

$F$

$\Sigma^0_1$$\Pi^0_2$

Das Erzwingen scheint derzeit für automatisierte Methoden weit außerhalb der Reichweite zu sein.