<p>I found signs that such a decision procedure was implemented in the (general purpose) theorem prover <a href="https://www.mpi-inf.mpg.de/departments/automation-of-logic/software/spass-workbench/classic-spass-theorem-prover/" rel="nofollow noreferrer">SPASS</a>. </p>

<p>In particular see the thesis of Ann-Christin Knoll, <a href="https://studentnet.cs.manchester.ac.uk/resources/library/thesis_abstracts/MSc15/FullText/Knoll-AnnChristin-diss.pdf" rel="nofollow noreferrer">On Resolution
Decision Procedures
for the Monadic Fragment and Guarded Negation
Fragment.</a> This implements what you want, though I couldn't find the implementation online.</p>

CC BY-SA 3.0
2017-11-09T17:50:45.270Z
2017-11-09T17:50:45.270Z
cody
<p>In a 1993 LICS paper, Bachmair, Ganzinger and Waldmann showed that set constraints are equivalent to monadic FOL, in <a href="http://ieeexplore.ieee.org/document/287598/?arnumber=287598" rel="nofollow noreferrer"><em>Set Constraints are the Monadic Class</em></a>. 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. </p>

<p>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.</p>

CC BY-SA 3.0
2017-11-09T19:37:59.797Z
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.
Joey Eremondi
CC BY-SA 3.0
2017-11-09T11:11:06.603Z
2017-11-09T11:11:06.603Z
Neel Krishnaswami
<p>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 <a href="http://www.sciencedirect.com/science/article/pii/0022000080900276" rel="noreferrer">NEXPTIME-complete</a>.</p>

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

<p>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?</p>

<reference-request><lo.logic><automated-theorem-proving><program-verification><first-order-logic>
State of the Art for the Monadic Class?
Joey Eremondi
# State of the Art for the Monadic Class?

(Asked by: username_0 on 2017-11-05)

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](http://www.sciencedirect.com/science/article/pii/0022000080900276).

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?

**Tags:** reference-request, lo.logic, automated-theorem-proving, program-verification, first-order-logic

---

## 2 answers

### Answer by username_1 on 2017-11-09. Score: 3 | Accepted answer

I found signs that such a decision procedure was implemented in the (general purpose) theorem prover [SPASS](https://www.mpi-inf.mpg.de/departments/automation-of-logic/software/spass-workbench/classic-spass-theorem-prover/).

In particular see the thesis of Ann-Christin Knoll, [On Resolution
Decision Procedures
for the Monadic Fragment and Guarded Negation
Fragment.](https://studentnet.cs.manchester.ac.uk/resources/library/thesis_abstracts/MSc15/FullText/Knoll-AnnChristin-diss.pdf) This implements what you want, though I couldn't find the implementation online.


---

### Answer by username_2 on 2017-11-09. Score: 3

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*](http://ieeexplore.ieee.org/document/287598/?arnumber=287598). 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.

> **Comments:**
> **username_0**: 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.  

---

