<p>There are <a href="https://people.mpi-inf.mpg.de/%7Ejblanche/nitpick.html" rel="nofollow noreferrer">Nitpick</a> and <a href="https://github.com/nunchaku-inria/nunchaku" rel="nofollow noreferrer">Nunchaku</a> that are model finders for higher-order logic.</p>
<p>Nunchaku is more recent and can build models for axioms containing higher-order quantification. But, as the problem is generally undecidable, it may not find a (finite) model even if one exists.</p>

CC BY-SA 4.0
2021-02-25T00:44:29.507Z
2021-02-25T00:44:29.507Z
selig
<p>I know that there are implementations of first-order (finite) satisfiability checking that, given a finite set of axioms, searches for a finite model that satisfies them all.</p>
<p>I would like to ask whether there is a second-order logic (finite) satisfiability checker. Although, we can always write a (naive) algorithm that enumerates all possible finite interpretations and check whether they are a model or not, I would like to know if there is some implementation/research doing something more intelligent (instead of a blind search).</p>

CC BY-SA 4.0
2020-10-17T19:02:29.533Z
Over which signatures? In general, both first-order and second-order logics are undecidable.
Shaull
CC BY-SA 4.0
2020-10-18T08:44:42.010Z
I was thinking over general signatures. That is, the signature is given as input into the finite satisfiability checker. Indeed, as you say, the problem is undecidable. Hence, to ensure termination, some of these tools limits the search scope (such as Alloy https://en.wikipedia.org/wiki/Alloy_(specification_language)). However, I think that Alloy only finds models over first-order theories, and cannot work with second-order constraints.
441Juggler
CC BY-SA 4.0
2020-10-18T08:51:27.927Z
I don't know of such tools. Maybe this question would be more appropriate at stackoverflow, they might know more about software tools.
Shaull
<finite-model-theory>
Is there any second-order logic finite satisfiability checker?
441Juggler
# Is there any second-order logic finite satisfiability checker?

(Asked by: username_0 on 2020-10-17)

I know that there are implementations of first-order (finite) satisfiability checking that, given a finite set of axioms, searches for a finite model that satisfies them all.

I would like to ask whether there is a second-order logic (finite) satisfiability checker. Although, we can always write a (naive) algorithm that enumerates all possible finite interpretations and check whether they are a model or not, I would like to know if there is some implementation/research doing something more intelligent (instead of a blind search).

**Tags:** finite-model-theory

> **Comments:**
> **username_1**: Over which signatures? In general, both first-order and second-order logics are undecidable.  
> **username_0**: I was thinking over general signatures. That is, the signature is given as input into the finite satisfiability checker. Indeed, as you say, the problem is undecidable. Hence, to ensure termination, some of these tools limits the search scope (such as Alloy https://en.wikipedia.org/wiki/Alloy_(specification_language)). However, I think that Alloy only finds models over first-order theories, and cannot work with second-order constraints.  
> **username_1**: I don't know of such tools. Maybe this question would be more appropriate at stackoverflow, they might know more about software tools.  

---

## 1 answers

### Answer by username_2 on 2021-02-25. Score: 2

There are [Nitpick](https://people.mpi-inf.mpg.de/%7Ejblanche/nitpick.html) and [Nunchaku](https://github.com/nunchaku-inria/nunchaku) that are model finders for higher-order logic.

Nunchaku is more recent and can build models for axioms containing higher-order quantification. But, as the problem is generally undecidable, it may not find a (finite) model even if one exists.


---

