1
$\begingroup$

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).

Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ Over which signatures? In general, both first-order and second-order logics are undecidable. $\endgroup$
    – Shaull
    Oct 17 '20 at 19:02
  • 1
    $\begingroup$ 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 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. $\endgroup$
    – 441Juggler
    Oct 18 '20 at 8:44
  • $\begingroup$ I don't know of such tools. Maybe this question would be more appropriate at stackoverflow, they might know more about software tools. $\endgroup$
    – Shaull
    Oct 18 '20 at 8:51
2
$\begingroup$

There are Nitpick and 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.

Improve this answer
$\endgroup$

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.