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

  • 1
    $\begingroup$ Over which signatures? In general, both first-order and second-order logics are undecidable. $\endgroup$ – Shaull Oct 17 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 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 at 8:51

Your Answer

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

Browse other questions tagged or ask your own question.