Stand der Technik für die Monadenklasse?

In der monadischen Logik erster Ordnung, auch als monadische Klasse des Entscheidungsproblems bekannt, nehmen alle Prädikate ein Argument an. Es wurde von Ackermann als entscheidbar erwiesen und ist NEXPTIME-vollständig .

Probleme wie SAT und SMT haben jedoch trotz der theoretischen Grenzen schnelle Algorithmen, um sie zu lösen.

Ich frage mich, gibt es Forschung analog zu SAT / SMT für monadische Logik erster Ordnung? Was ist in diesem Fall der "Stand der Technik", und gibt es Algorithmen, die in der Praxis effizient sind, obwohl sie im schlimmsten Fall an die theoretischen Grenzen stoßen?

Ich fand Anzeichen dafür, dass ein solches Entscheidungsverfahren im (allgemeinen) Theorembeweiser SPASS implementiert wurde .

Siehe insbesondere die These von Ann-Christin Knoll über Auflösungsentscheidungsverfahren für das monadische Fragment und das Fragment der bewachten Negation. Dies implementiert, was Sie wollen, obwohl ich die Implementierung online nicht finden konnte.

In einem LICS-Papier von 1993 zeigten Bachmair, Ganzinger und Waldmann, dass Mengenbeschränkungen der monadischen FOL entsprechen, in Mengenbeschränkungen die monadische Klasse . Wenn Speicher dient, entsprechen festgelegte Einschränkungen regulären Baumgrammatiken, sodass die meisten der dort entwickelten Algorithmen auch auf monadische FOL portierbar sein sollten.

Ich kenne den Bereich nicht so gut, aber festgelegte Einschränkungen und reguläre Baumgrammatiken wurden in der Programmanalyse ausgiebig verwendet, daher sollte an praktischen Algorithmen für sie gearbeitet werden.