=Paper=
{{Paper
|id=Vol-2013/paper7
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-2013/paper7.pdf
|volume=Vol-2013
}}
==None==
https://ceur-ws.org/Vol-2013/paper7.pdf
13
Swinging between Expressiveness and Complexity
in Second-Order Formalisms: A Case Study
(Abstract of Invited Talk)
Andrzej Szałas1,2
1
Institute of Informatics, University of Warsaw, Poland
2
Department of Computer and Information Science, Linköping University, Sweden
andrzej.szalas@{mimuw.edu.pl,liu.se}
Second-order logic proved very useful in formalizing phenomena related to many
forms of reasoning both monotonic and nonmonotonic. One of the misconcep-
tions 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 circum-
scription [2,8] and many others [6].
When modeling complex phenomena, like those related to commonsense rea-
soning, 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 gen-
eral (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 elim-
ination [2,8] This approach is also applied in [3] where a technique for comput-
ing weakest sufficient and strongest necessary conditions for first-order theories
using second-order quantifier elimination is provided. Given a theory express-
ing 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 al-
lows 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 con-
straints. 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.
Copyright c 2017 by the paper’s authors
In: P. Koopmann, S. Rudolph, R. Schmidt, C. Wernhard (eds.): SOQE 2017 – Pro-
ceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics,
Dresden, Germany, December 6–8, 2017, published at http://ceur-ws.org.
14
References
1. Conradie, W., Goranko, V., Vakarelov, D.: Algorithmic correspondence and com-
pleteness in modal logic: I. the core algorithm SQEMA. Logical Methods in Com-
puter Science 2(1:5), 1–26 (2006)
2. Doherty, P., Łukaszewicz, W., Szałas, A.: Computing circumscription revisited: A
reduction algorithm. J. Autom. Reasoning 18(3), 297–336 (1997)
3. Doherty, P., Łukaszewicz, W., Szałas, A.: Computing strongest necessary and weak-
est sufficient conditions of first-order formulas. In: Nebel, B. (ed.) Proc 17th IJCAI:
Int. Joint Conf. on AI. pp. 145 – 151 (2001)
4. Doherty, P., Szałas, A.: Reasoning with qualitative preferences and cardinalities
using generalized circumscription. In: Brewka, G., Lang, J. (eds.) Proc. 11th Conf.
KR: Principles of Knowledge Representation and Reasoning. pp. 560–570. AAAI
Press (2008)
5. Gabbay, D.M., Ohlbach, H.J.: Quantifier elimination in second-order predicate
logic. South African Computer Journal 7, 35–43 (1992)
6. Gabbay, D., Schmidt, R., Szałas, A.: Second-Order Quantifier Elimination. Foun-
dations, Computational Aspects and Applications, Studies in Logic, vol. 12. College
Publications (2008)
7. Lifschitz, V.: Some results on circumscription. In: Proc. 1st AAAI Workshop on
Nonmonotonic Reasoning. pp. 151–164 (1984)
8. Lifschitz, V.: Circumscription. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A.
(eds.) Handbook of Artificial Intelligence and Logic Programming. vol. 3, pp. 297–
352. Oxford University Press (1991)
9. Lin, F.: On strongest necessary and weakest sufficient conditions. In: Cohn, A.,
Giunchiglia, F., Selman, B. (eds.) Proc. 7th Conf. KR: Principles of Knowledge
Representation and Reasoning. pp. 167–175. Morgan Kaufmann Pub., Inc. (2000)
10. Nonnengart, A., Szałas, A.: A fixpoint approach to second-order quantifier elimi-
nation with applications to correspondence theory. In: Orłowska, E. (ed.) Logic at
Work: Essays Dedicated to the Memory of Helena Rasiowa. Studies in Fuzziness
and Soft Computing, vol. 24, pp. 307–328. Springer (1998)
11. Sahlqvist, H.: Correspondence and completeness in the first- and second-order se-
mantics for modal logic. In: Kanger, S. (ed.) Proc. 3rd Scandinavial Logic Sympo-
sium. pp. 110–143. North-Holland, Amsterdam (1975)
12. Szałas, A.: On the correspondence between modal and classical logic: An auto-
mated approach. Journal of Logic and Computation 3, 605–620 (1993)
13. Szałas, A.: Second-order reasoning in description logics. Journal of Applied Non-
Classical Logics 16(3-4), 517–530 (2006)
14. vanBenthem, J.: Correspondence theory. In: Gabbay, D.M., Guenthner, F. (eds.)
Handbook of Philosophical Logic. vol. 2, pp. 167–247. D. Reidel Pub. Co. (1984)
15. Wernhard, C.: Second-order quantifier elimination on relational monadic formulas
– A basic method and some less expected applications. In: de Nivelle, H. (ed.)
Proc. 24th Int. Conf. TABLEAUX 2015. LNCS (LNAI), vol. 9323, pp. 249–265.
Springer (2015)
16. Zhao, Y., Schmidt, R.: Role forgetting for ALCOQH(universal role)-ontologies us-
ing an Ackermann-based approach. In: Sierra, C. (ed.) Proc. 26th IJCAI: Int. Joint
Conf. on AI. pp. 1354–1361 (2017)