Semi-Entscheidbarkeit der Prädikatenlogik

Es gibt einen Algorithmus der auf eine willkürliche prädikatenlogische Formel angesetzt werden kann und mit ja terminiert, wenn die Formel allgemeingültig ist.

Ein solches semi-entscheidbares Verfahren, dass terminiert wenn die Formel unerfüllbar ist, ist die Grundresolution. Also gibt es ein semi-entscheidbares Verfahren für die Allgemeingültigkeit prädikatenlogischer Formeln.