12
$\begingroup$

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?

Improve this question
$\endgroup$

2 Answers 2

Reset to default
3
+50
$\begingroup$

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.

Improve this answer
$\endgroup$
3
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • $\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$
    – Joey Eremondi
    Nov 9, 2017 at 19:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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