4
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 $\...
2
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