{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T21:07:46Z","timestamp":1725829666337},"publisher-location":"Cham","reference-count":48,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319243115"},{"type":"electronic","value":"9783319243122"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24312-2_18","type":"book-chapter","created":{"date-parts":[[2015,9,10]],"date-time":"2015-09-10T10:06:46Z","timestamp":1441879606000},"page":"253-269","source":"Crossref","is-referenced-by-count":3,"title":["Second-Order Quantifier Elimination on Relational Monadic Formulas \u2013 A Basic Method and Some Less Expected Applications"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Wernhard","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,8]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/BF01448035","volume":"110","author":"W. Ackermann","year":"1935","unstructured":"Ackermann, W.: Untersuchungen \u00fcber das Eliminationsproblem der mathematischen Logik. Math. Ann.\u00a0110, 390\u2013413 (1935)","journal-title":"Math. Ann."},{"key":"18_CR2","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/BF01472201","volume":"111","author":"W. Ackermann","year":"1935","unstructured":"Ackermann, W.: Zum Eliminationsproblem der mathematischen Logik. Math. Ann.\u00a0111, 61\u201363 (1935)","journal-title":"Math. Ann."},{"key":"18_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1613\/jair.2820","volume":"36","author":"A. Artale","year":"2009","unstructured":"Artale, A., Calvanese, D., Kontchakov, R., Zakharyaschev, M.: The DL-Lite family and relations. JAIR\u00a036, 1\u201369 (2009)","journal-title":"JAIR"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/BFb0022557","volume-title":"Computational Logic and Proof Theory","author":"L. Bachmair","year":"1993","unstructured":"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.\u00a0713, pp. 83\u201396. Springer, Heidelberg (1993)"},{"issue":"3\u20134","key":"18_CR5","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/BF01457985","volume":"86","author":"H. Behmann","year":"1922","unstructured":"Behmann, H.: Beitr\u00e4ge zur Algebra der Logik, insbesondere zum Entscheidungsproblem. Math. Ann.\u00a086(3\u20134), 163\u2013229 (1922)","journal-title":"Math. Ann."},{"key":"18_CR6","unstructured":"Behmann, H. (Bestandsbildner): Nachlass Heinrich Johann Behmann, Staatsbibliothek zu Berlin \u2013 Preu\u00dfischer Kulturbesitz, Handschriftenabt., Nachl. 335"},{"key":"18_CR7","unstructured":"van Benthem, J.: Modal Logic and Classical Logic. Bibliopolis (1983)"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Blackburn, P., de\u00a0Rijke, M., Venema, Y.: Modal Logic. Cambr. Univ. Press (2001)","DOI":"10.1017\/CBO9781107050884"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem. Springer (1997)","DOI":"10.1007\/978-3-642-59207-2"},{"issue":"3","key":"18_CR10","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/s10817-007-9078-x","volume":"39","author":"D. Calvanese","year":"2007","unstructured":"Calvanese, D., et al.: Tractable reasoning and efficient query answering in description logics: The DL-Lite family. JAR\u00a039(3), 385\u2013429 (2007)","journal-title":"JAR"},{"issue":"3\u20134","key":"18_CR11","first-page":"279","volume":"16","author":"W. Conradie","year":"2006","unstructured":"Conradie, W.: On the strength and scope of DLS. JANCL\u00a016(3\u20134), 279\u2013296 (2006)","journal-title":"JANCL"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Conradie, W., Goranko, V., Vakarelov, D.: Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA. LMCS 2(1:5), 1\u201326 (2006)","DOI":"10.2168\/LMCS-2(1:5)2006"},{"key":"18_CR13","unstructured":"Conradie, W., Goranko, V., Vakarelov, D.: Elementary canonical formulae: A survey on syntactic, algorithmic, and model-theoretic aspects. In: Advances in Modal Logic, vol.\u00a05, pp. 17\u201351. College Pub. (2005)"},{"key":"18_CR14","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/s11229-008-9352-4","volume":"164","author":"W. Craig","year":"2008","unstructured":"Craig, W.: Elimination problems in logic: A brief history. Synthese\u00a0164, 321\u2013332 (2008)","journal-title":"Synthese"},{"issue":"3","key":"18_CR15","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1023\/A:1005722130532","volume":"18","author":"P. Doherty","year":"1997","unstructured":"Doherty, P., \u0141ukaszewicz, W., Sza\u0142as, A.: Computing circumscription revisited: A reduction algorithm. JAR\u00a018(3), 297\u2013338 (1997)","journal-title":"JAR"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/3-540-58216-9_30","volume-title":"Logic Programming and Automated Reasoning","author":"U. Egly","year":"1994","unstructured":"Egly, U.: On the value of antiprenexing. In: Pfenning, F. (ed.) LPAR 1994. LNCS, vol.\u00a0822, pp. 69\u201383. Springer, Heidelberg (1994)"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Ferm\u00fcller, C., Leitsch, A., Hustadt, U., Tammet, T.: Resolution decision procedures. In: Robinson, A., Voronkov, A. (eds.) Handb. of Autom. Reasoning, vol.\u00a02, pp. 1793\u20131849. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50027-8"},{"key":"18_CR18","unstructured":"Gabbay, D.M., Schmidt, R.A., Sza\u0142as, A.: Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. College Pub. (2008)"},{"key":"18_CR19","unstructured":"Gabbay, D., Ohlbach, H.J.: Quantifier elimination in second-order predicate logic. In: KR 1992, pp. 425\u2013435. Morgan Kaufmann (1992)"},{"key":"18_CR20","unstructured":"Ghilardi, S., Lutz, C., Wolter, F.: Did I damage my ontology? A case for conservative extensions in description logics. In: KR 2006, pp. 187\u2013197. AAAI Press (2006)"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-24771-5_13","volume-title":"Relational and Kleene-Algebraic Methods in Computer Science","author":"V. Goranko","year":"2004","unstructured":"Goranko, V., Hustadt, U., Schmidt, R.A., Vakarelov, D.: SCAN is complete for all Sahlqvist formulae. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol.\u00a03051, pp. 149\u2013162. Springer, Heidelberg (2004)"},{"key":"18_CR22","unstructured":"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\u00f6ping (1996)"},{"key":"18_CR23","first-page":"251","volume":"1","author":"U. Hustadt","year":"2004","unstructured":"Hustadt, U., Schmidt, R.A., Georgieva, L.: A survey of decidable first-order fragments and description logics. JoRMiCS\u00a01, 251\u2013276 (2004)","journal-title":"JoRMiCS"},{"key":"18_CR24","unstructured":"Konev, B., Walther, D., Wolter, F.: Forgetting and uniform interpolation in large-scale description logic terminologies. In: IJCAI 2009, pp. 830\u2013835 (2009)"},{"issue":"15","key":"18_CR25","first-page":"1093","volume":"174","author":"R. Kontchakov","year":"2010","unstructured":"Kontchakov, R., Wolter, F., Zakharyaschev, M.: Logic-based ontology comparison and module extraction, with an application to DL-Lite. AI\u00a0174(15), 1093\u20131141 (2010)","journal-title":"AI"},{"key":"18_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-642-40885-4_7","volume-title":"Frontiers of Combining Systems","author":"P. Koopmann","year":"2013","unstructured":"Koopmann, P., Schmidt, R.A.: Uniform interpolation of \n                      \n                        \n                      \n                      $\\mathcal{ALC}$\n                    -ontologies using fixpoints. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS, vol.\u00a08152, pp. 87\u2013102. Springer, Heidelberg (2013)"},{"key":"18_CR27","series-title":"LNCS (LNAI)","doi-asserted-by":"crossref","first-page":"434","DOI":"10.1007\/978-3-319-08587-6_34","volume-title":"Automated Reasoning","author":"P. Koopmann","year":"2014","unstructured":"Koopmann, P., Schmidt, R.A.: Count and forget: Uniform interpolation of\u00a0\n                      \n                        \n                      \n                      $\\mathcal{SHQ}$\n                    -ontologies. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol.\u00a08562, pp. 434\u2013448. Springer, Heidelberg (2014)"},{"key":"18_CR28","unstructured":"Koopmann, P., Schmidt, R.A.: Uniform interpolation and forgetting for \n                      \n                        \n                      \n                      $\\mathcal{ALC}$\n                     ontologies with ABoxes. In: AAAI 2015, pp. 175\u2013181. AAAI Press (2015)"},{"key":"18_CR29","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0022-0000(80)90027-6","volume":"21","author":"H.R. Lewis","year":"1980","unstructured":"Lewis, H.R.: Complexity results for classes of quantificational formulas. Journal of Computer and System Sciences\u00a021, 317\u2013353 (1980)","journal-title":"Journal of Computer and System Sciences"},{"key":"18_CR30","unstructured":"Ludwig, M., Konev, B.: Practical uniform interpolation and forgetting for \n                      \n                        \n                      \n                      $\\mathcal{ALC}$\n                     TBoxes with applications to logical difference. In: KR 2014. AAAI Press (2014)"},{"key":"18_CR31","unstructured":"Lutz, C., Wolter, F.: Foundations for uniform interpolation and forgetting in expressive description logics. In: IJCAI 2011, pp. 989\u2013995. AAAI Press (2011)"},{"key":"18_CR32","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/BF01458217","volume":"76","author":"L. L\u00f6wenheim","year":"1915","unstructured":"L\u00f6wenheim, L.: \u00dcber M\u00f6glichkeiten im Relativkalk\u00fcl. Math. Ann.\u00a076, 447\u2013470 (1915)","journal-title":"Math. Ann."},{"key":"18_CR33","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1017\/bsl.2015.10","volume":"21","author":"P. Mancosu","year":"2015","unstructured":"Mancosu, P., Zach, R.: Heinrich Behmann\u2019s 1921 lecture on the algebra of logic and the decision problem. The Bulletin of Symbolic Logic\u00a021, 164\u2013187 (2015)","journal-title":"The Bulletin of Symbolic Logic"},{"key":"18_CR34","series-title":"LNCS (LNAI)","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-540-45206-5_14","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"N.V. Murray","year":"2003","unstructured":"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.\u00a02796, pp. 165\u2013180. Springer, Heidelberg (2003)"},{"key":"18_CR35","unstructured":"Nonnengart, A., Sza\u0142as, 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\u2013108. Springer (1998)"},{"key":"18_CR36","doi-asserted-by":"crossref","unstructured":"Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, A., Voronkov, A. (eds.) Handb. of Autom. Reasoning, vol.\u00a01, pp. 335\u2013367. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50008-4"},{"issue":"1","key":"18_CR37","first-page":"1","volume":"10","author":"W.V. Quine","year":"1945","unstructured":"Quine, W.V.: On the logic of quantification. JSL\u00a010(1), 1\u201312 (1945)","journal-title":"JSL"},{"key":"18_CR38","unstructured":"Sattler, U., Calvanese, D., Molitor, R.: Relationships with other formalisms. In: Baader, F., et al. (eds.) The Description Logic Handb, pp. 137\u2013177. Cambr. Univ. Press (2003)"},{"issue":"1","key":"18_CR39","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1016\/j.jal.2012.01.001","volume":"10","author":"R.A. Schmidt","year":"2012","unstructured":"Schmidt, R.A.: The Ackermann approach for modal logic, correspondence theory and second-order reduction. JAL\u00a010(1), 52\u201374 (2012)","journal-title":"JAL"},{"key":"18_CR40","doi-asserted-by":"crossref","unstructured":"Schneider, K.: Verification of Reactive Systems. Springer (2003)","DOI":"10.1007\/978-3-662-10778-2"},{"key":"18_CR41","unstructured":"Skolem, T.: Untersuchungen \u00fcber die Axiome des Klassenkalk\u00fcls und \u00fcber Produktations- und Summationsprobleme welche gewisse Klassen von Aussagen betreffen. Videnskapsselskapets Skrifter I. Mat.-Nat. Klasse(3) (1919)"},{"key":"18_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"628","DOI":"10.1007\/978-3-319-08867-9_42","volume-title":"Computer Aided Verification","author":"M. Veanes","year":"2014","unstructured":"Veanes, M., Bj\u00f8rner, N., Nachmanson, L., Bereg, S.: Monadic decomposition. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol.\u00a08559, pp. 628\u2013645. Springer, Heidelberg (2014)"},{"key":"18_CR43","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/s10472-010-9187-9","volume":"58","author":"Z. Wang","year":"2010","unstructured":"Wang, Z., Wang, K., Topor, R.W., Pan, J.Z.: Forgetting for knowledge bases in DL-Lite. Ann. Math. Artif. Intell.\u00a058, 117\u2013151 (2010)","journal-title":"Ann. Math. Artif. Intell."},{"key":"18_CR44","series-title":"LNCS (LNAI)","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-642-02716-1_24","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"C. Wernhard","year":"2009","unstructured":"Wernhard, C.: Tableaux for projection computation and knowledge compilation. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS (LNAI), vol.\u00a05607, pp. 325\u2013340. Springer, Heidelberg (2009)"},{"key":"18_CR45","series-title":"LNCS (LNAI)","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-40885-4_8","volume-title":"Frontiers of Combining Systems","author":"C. Wernhard","year":"2013","unstructured":"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.\u00a08152, pp. 103\u2013119. Springer, Heidelberg (2013)"},{"key":"18_CR46","unstructured":"Wernhard, C.: Expressing view-based query processing and related approaches with second-order operators. Tech. Rep. KRR 14\u201302, TU Dresden (2014)"},{"key":"18_CR47","unstructured":"Wernhard, C.: Heinrich Behmann\u2019s contributions to second-order quantifier elimination. Tech. Rep. KRR 15\u201305, TU Dresden (2015)"},{"key":"18_CR48","doi-asserted-by":"crossref","unstructured":"Wernhard, C.: Second-order quantifier elimination on relational monadic formulas \u2013 A basic method and some less expected applications. Tech. Rep. KRR 15\u201304, TU Dresden (2015)","DOI":"10.1007\/978-3-319-24312-2_18"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24312-2_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T19:00:37Z","timestamp":1559242837000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24312-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243115","9783319243122"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24312-2_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}