  We analyze possibilities of second-order quantifier elimination for formulae
containing parameters -- constants or functions. For this, we use a constraint
resolution calculus obtained from specializing the hierarchical superposition
calculus. If saturation terminates, we analyze possibilities of obtaining
weakest constraints on parameters which guarantee satisfiability. If the
saturation does not terminate, we identify situations in which finite
representations of infinite saturated sets exist. We identify situations in
which entailment between formulae expressed using second-order quantification
can be effectively checked. We illustrate the ideas on a series of examples
from wireless network research.
