Let us use the modal logic example to illustrate how SCAN can be used for computing the corresponding frame properties. Suppose we are given the Hilbert axiom []p ->p and the standard possible worlds semantics of the modal operator:
When using SCAN for computing the corresponding frame property for a given Hilbert axiom, four different things may happen.
We cannot guarantee is that there is no first-order formula which is equivalent to this second-order formula. (The unskolemization is a quite sophisticated search process which is not guaranteed to find all possible unskolemization possibilities.)
In modal logic it is known that the conjunction of the Mc Kinsey axiom together with the axiom []p -> [][]p, which specifies transitivity of the accessibility relation, correspond to the atomicity of the frames: all x exists y r(x,y) & all z r(y,z) -> y = z. For the current version of SCAN there is no way to find this out. SCAN would compute the Mc Kinsey axiom and then transitivity axiom separately and not relate the conjunction with atomicity.
That means the computation of correspondence properties for conjunctions of Hilbert axioms may not give the optimal result.