Consider a universe with two elements 0,1 and a second order formula, i.e. of the form "forall R exists S ... such that F", where R,S are relation symbols of some given arity, and F is some first order formula e.g. "exists x forall y R(x,y)&S(y,x)".

Further for simplicity assume that the quantifier-free part (the "matrix") of F is given in disjunctive normal form, and everything is in prenex normal form.

What would be an algorithm to decide satisfiability (or better, list all solutions namely if the formula begins with "exists R" to list all relations that satisfy it) of such second order boolean formula, anything better than brute force in the average case (as probably no one knows to do it better than brute force in the worst case if that's even possible)? Surely just a reference would be great as well.

Alternatively, if one can point me to a second-order version of the resolution method.


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.