I don't know of any natural logic, but the following is in any case a logic for which the combined complexity of the model-checking problem is different for matrix and list encodings. First, we know that for every QBF formula $\psi$ there exists a sentence $\varphi_\psi$ of FO over the vocabulary $\{P\}$, where $P$ is unary, such that $\psi$ is true iff $\...


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.

Only top voted, non community-wiki answers of a minimum length are eligible