Abstract
For relational monadic formulas (the Löwenheim class) second-order quantifier elimination, which is closely related to computation of uniform interpolants, forgetting and projection, always succeeds. The decidability proof for this class by Behmann from 1922 explicitly proceeds by elimination with equivalence preserving formula rewriting. We reconstruct Behmann’s method, relate it to the modern DLS elimination algorithm and show some applications where the essential monadicity becomes apparent only at second sight. In particular, deciding \(\mathcal{ALCOQH}\) knowledge bases, elimination in DL-Lite knowledge bases, and the justification of the success of elimination methods for Sahlqvist formulas.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Ackermann, W.: Untersuchungen über das Eliminationsproblem der mathematischen Logik. Math. Ann. 110, 390–413 (1935)
Ackermann, W.: Zum Eliminationsproblem der mathematischen Logik. Math. Ann. 111, 61–63 (1935)
Artale, A., Calvanese, D., Kontchakov, R., Zakharyaschev, M.: The DL-Lite family and relations. JAIR 36, 1–69 (2009)
Bachmair, L., Ganzinger, H., Waldmann, U.: Superposition with simplification as a decision procedure for the monadic class with equality. In: Mundici, D., Gottlob, G., Leitsch, A. (eds.) KGC 1993. LNCS, vol. 713, pp. 83–96. Springer, Heidelberg (1993)
Behmann, H.: Beiträge zur Algebra der Logik, insbesondere zum Entscheidungsproblem. Math. Ann. 86(3–4), 163–229 (1922)
Behmann, H. (Bestandsbildner): Nachlass Heinrich Johann Behmann, Staatsbibliothek zu Berlin – Preußischer Kulturbesitz, Handschriftenabt., Nachl. 335
van Benthem, J.: Modal Logic and Classical Logic. Bibliopolis (1983)
Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambr. Univ. Press (2001)
Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. Springer (1997)
Calvanese, D., et al.: Tractable reasoning and efficient query answering in description logics: The DL-Lite family. JAR 39(3), 385–429 (2007)
Conradie, W.: On the strength and scope of DLS. JANCL 16(3–4), 279–296 (2006)
Conradie, W., Goranko, V., Vakarelov, D.: Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA. LMCS 2(1:5), 1–26 (2006)
Conradie, W., Goranko, V., Vakarelov, D.: Elementary canonical formulae: A survey on syntactic, algorithmic, and model-theoretic aspects. In: Advances in Modal Logic, vol. 5, pp. 17–51. College Pub. (2005)
Craig, W.: Elimination problems in logic: A brief history. Synthese 164, 321–332 (2008)
Doherty, P., Łukaszewicz, W., Szałas, A.: Computing circumscription revisited: A reduction algorithm. JAR 18(3), 297–338 (1997)
Egly, U.: On the value of antiprenexing. In: Pfenning, F. (ed.) LPAR 1994. LNCS, vol. 822, pp. 69–83. Springer, Heidelberg (1994)
Fermüller, C., Leitsch, A., Hustadt, U., Tammet, T.: Resolution decision procedures. In: Robinson, A., Voronkov, A. (eds.) Handb. of Autom. Reasoning, vol. 2, pp. 1793–1849. Elsevier (2001)
Gabbay, D.M., Schmidt, R.A., Szałas, A.: Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. College Pub. (2008)
Gabbay, D., Ohlbach, H.J.: Quantifier elimination in second-order predicate logic. In: KR 1992, pp. 425–435. Morgan Kaufmann (1992)
Ghilardi, S., Lutz, C., Wolter, F.: Did I damage my ontology? A case for conservative extensions in description logics. In: KR 2006, pp. 187–197. AAAI Press (2006)
Goranko, V., Hustadt, U., Schmidt, R.A., Vakarelov, D.: SCAN is complete for all Sahlqvist formulae. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol. 3051, pp. 149–162. Springer, Heidelberg (2004)
Gustafsson, J.: An implementation and optimization of an algorithm for reducing formulae in second-order logic. Tech. Rep. LiTH-MAT-R-96-04, Univ. Linköping (1996)
Hustadt, U., Schmidt, R.A., Georgieva, L.: A survey of decidable first-order fragments and description logics. JoRMiCS 1, 251–276 (2004)
Konev, B., Walther, D., Wolter, F.: Forgetting and uniform interpolation in large-scale description logic terminologies. In: IJCAI 2009, pp. 830–835 (2009)
Kontchakov, R., Wolter, F., Zakharyaschev, M.: Logic-based ontology comparison and module extraction, with an application to DL-Lite. AI 174(15), 1093–1141 (2010)
Koopmann, P., Schmidt, R.A.: Uniform interpolation of \(\mathcal{ALC}\)-ontologies using fixpoints. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS, vol. 8152, pp. 87–102. Springer, Heidelberg (2013)
Koopmann, P., Schmidt, R.A.: Count and forget: Uniform interpolation of \(\mathcal{SHQ}\)-ontologies. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 434–448. Springer, Heidelberg (2014)
Koopmann, P., Schmidt, R.A.: Uniform interpolation and forgetting for \(\mathcal{ALC}\) ontologies with ABoxes. In: AAAI 2015, pp. 175–181. AAAI Press (2015)
Lewis, H.R.: Complexity results for classes of quantificational formulas. Journal of Computer and System Sciences 21, 317–353 (1980)
Ludwig, M., Konev, B.: Practical uniform interpolation and forgetting for \(\mathcal{ALC}\) TBoxes with applications to logical difference. In: KR 2014. AAAI Press (2014)
Lutz, C., Wolter, F.: Foundations for uniform interpolation and forgetting in expressive description logics. In: IJCAI 2011, pp. 989–995. AAAI Press (2011)
Löwenheim, L.: Über Möglichkeiten im Relativkalkül. Math. Ann. 76, 447–470 (1915)
Mancosu, P., Zach, R.: Heinrich Behmann’s 1921 lecture on the algebra of logic and the decision problem. The Bulletin of Symbolic Logic 21, 164–187 (2015)
Murray, N.V., Rosenthal, E.: Tableaux, path dissolution and decomposable negation normal form for knowledge compilation. In: Cialdea Mayer, M., Pirri, F. (eds.) TABLEAUX 2003. LNCS (LNAI), vol. 2796, pp. 165–180. Springer, Heidelberg (2003)
Nonnengart, A., Szałas, A.: A fixpoint approach to second-order quantifier elimination with applications to correspondence theory. In: Orlowska, E. (ed.) Logic at Work. Essays Ded. to the Mem. of Helena Rasiowa, pp. 89–108. Springer (1998)
Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, A., Voronkov, A. (eds.) Handb. of Autom. Reasoning, vol. 1, pp. 335–367. Elsevier (2001)
Quine, W.V.: On the logic of quantification. JSL 10(1), 1–12 (1945)
Sattler, U., Calvanese, D., Molitor, R.: Relationships with other formalisms. In: Baader, F., et al. (eds.) The Description Logic Handb, pp. 137–177. Cambr. Univ. Press (2003)
Schmidt, R.A.: The Ackermann approach for modal logic, correspondence theory and second-order reduction. JAL 10(1), 52–74 (2012)
Schneider, K.: Verification of Reactive Systems. Springer (2003)
Skolem, T.: Untersuchungen über die Axiome des Klassenkalküls und über Produktations- und Summationsprobleme welche gewisse Klassen von Aussagen betreffen. Videnskapsselskapets Skrifter I. Mat.-Nat. Klasse(3) (1919)
Veanes, M., Bjørner, N., Nachmanson, L., Bereg, S.: Monadic decomposition. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 628–645. Springer, Heidelberg (2014)
Wang, Z., Wang, K., Topor, R.W., Pan, J.Z.: Forgetting for knowledge bases in DL-Lite. Ann. Math. Artif. Intell. 58, 117–151 (2010)
Wernhard, C.: Tableaux for projection computation and knowledge compilation. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS (LNAI), vol. 5607, pp. 325–340. Springer, Heidelberg (2009)
Wernhard, C.: Abduction in logic programming as second-order quantifier elimination. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 103–119. Springer, Heidelberg (2013)
Wernhard, C.: Expressing view-based query processing and related approaches with second-order operators. Tech. Rep. KRR 14–02, TU Dresden (2014)
Wernhard, C.: Heinrich Behmann’s contributions to second-order quantifier elimination. Tech. Rep. KRR 15–05, TU Dresden (2015)
Wernhard, C.: Second-order quantifier elimination on relational monadic formulas – A basic method and some less expected applications. Tech. Rep. KRR 15–04, TU Dresden (2015)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Wernhard, C. (2015). Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications. In: De Nivelle, H. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2015. Lecture Notes in Computer Science(), vol 9323. Springer, Cham. https://doi.org/10.1007/978-3-319-24312-2_18
Download citation
DOI: https://doi.org/10.1007/978-3-319-24312-2_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24311-5
Online ISBN: 978-3-319-24312-2
eBook Packages: Computer ScienceComputer Science (R0)