-
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.