Second-order logic proved very useful in formalizing phenomena related to many forms of reasoning both monotonic and nonmonotonic. One of the misconceptions about various forms of second-order formalisms is that, in general, they are not amenable to practical use due to their high complexity. In fact, it is often the case that restricted, but quite general uses of second-order quantifier elimination allow for the constructive reduction of such second-order theories to logically equivalent first-order or fixpoint theories, as shown in many cases, e.g., in correspondence theory for modal logics [1,5,10,11,12,14], computing circumscription [2,8] and many others [6].

When modeling complex phenomena, like those related to commonsense reasoning, it proved useful to first swing up to the general case, using as complex logical tools as needed, and then to swing down by isolating fragments of general (second-or higher-order) theories admitting efficient reasoning techniques. This is evident, e.g., in the case of circumscription where the general case is second-order while large classes of formulas admit second-order quantifier elimination [2,8] This approach is also applied in [3] where a technique for computing weakest sufficient and strongest necessary conditions for first-order theories using second-order quantifier elimination is provided. Given a theory expressing properties of concepts, these conditions, proposed for the propositional case in [9], allow one to define the best approximations of concepts under the theory, assuming that some concepts have to be forgotten.

In [4], a highly expressive framework for qualitative preference modeling has been introduced. The framework uses generalized circumscription [7] which allows for predicates (and thus formulas) to be minimized/maximized relative to arbitrary pre-orders (reflexive and transitive). It has also been shown in [4] how a large variety of preference theories extended with cardinality constraints, can in fact be reduced to logically equivalent first-order theories using second-order quantifier elimination techniques developed for that purpose. This talk will be devoted to a case study of combining the techniques of [3,4] to swing up to a powerful higher-order formalism for approximating concepts when the underlying theories contain qualitative preferences and cardinality constraints. Then. suitable techniques and restrictions of the general theory will be indicated to swing down to computationally friendly cases. Of course, using techniques extending [13] (or, e.g., [15,16]), one can embed this formalism in description logics using suitable second-order quantifier elimination techniques. This will also be demonstrated during the talk.