Monadic First Order Logic, also known as the Monadic Class of the Decision Problem, is where all predicates take one argument. It was shown to be decidable by Ackermann, and is NEXPTIME-complete.

However, problems like SAT and SMT have fast algorithms for solving them, despite the theoretical bounds.

I'm wondering, is there research analogous to SAT/SMT for monadic first order logic? What is the "state of the art" in this case, and are there algorithms which are efficient in practice, despite hitting the theoretical limits in the worst case?


I found signs that such a decision procedure was implemented in the (general purpose) theorem prover SPASS.

In particular see the thesis of Ann-Christin Knoll, On Resolution Decision Procedures for the Monadic Fragment and Guarded Negation Fragment. This implements what you want, though I couldn't find the implementation online.


In a 1993 LICS paper, Bachmair, Ganzinger and Waldmann showed that set constraints are equivalent to monadic FOL, in Set Constraints are the Monadic Class. If memory serves, set constraints are equivalent to regular tree grammars, so most of the algorithms developed there should portable to monadic FOL as well.

I don't know the area that well, but set constraints and regular tree grammars have been used extensively in program analysis, so there should be work on practical algorithms for them.

  • $\begingroup$ Yeah... I'll admit my interest in the monadic class is in solving set constraints, so we've got a kind of chicken and egg problem. Most of what I've found for set constraints in program analysis, like Banshee, is of restricted classes that are weaker than the monadic class (i.e. they don't have negation or projection). But I could be missing a bunch. $\endgroup$
    – jmite
    Nov 9 '17 at 19:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.