Estado da arte para a classe monádica?

A lógica monádica de primeira ordem, também conhecida como classe monádica do problema de decisão, é onde todos os predicados usam um argumento. Foi demonstrado ser decidível por Ackermann e está NEXPTIME-complete .

No entanto, problemas como SAT e SMT têm algoritmos rápidos para resolvê-los, apesar dos limites teóricos.

Gostaria de saber, há pesquisas análogas ao SAT / SMT para lógica monádica de primeira ordem? Qual é o "estado da arte" neste caso, e existem algoritmos eficazes na prática, apesar de atingir os limites teóricos no pior caso?

Encontrei sinais de que esse procedimento de decisão foi implementado no provador de teoremas (de uso geral) SPASS .

Em particular, veja a tese de Ann-Christin Knoll, Procedimentos de decisão sobre resolução para o fragmento monádico e fragmento de negação guardada. Isso implementa o que você deseja, embora eu não tenha encontrado a implementação online.

Em um artigo do LICS de 1993, Bachmair, Ganzinger e Waldmann mostraram que restrições de conjunto são equivalentes a FOL monádicas, em Restrições de conjunto são a classe monádica . Se a memória serve, as restrições definidas são equivalentes às gramáticas regulares das árvores; portanto, a maioria dos algoritmos desenvolvidos lá também deve ser portável para FOL monádico.

Não conheço bem a área, mas restrições de conjunto e gramáticas regulares de árvores foram amplamente utilizadas na análise de programas, portanto, deve haver trabalho em algoritmos práticos para elas.