{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,21]],"date-time":"2026-03-21T02:34:35Z","timestamp":1774060475428,"version":"3.50.1"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319661667","type":"print"},{"value":"9783319661674","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66167-4_19","type":"book-chapter","created":{"date-parts":[[2017,8,28]],"date-time":"2017-08-28T11:15:18Z","timestamp":1503918918000},"page":"333-350","source":"Crossref","is-referenced-by-count":6,"title":["The Boolean Solution Problem from the Perspective of Predicate Logic"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Wernhard","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,29]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","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. 110, 390\u2013413 (1935)","journal-title":"Math. Ann."},{"issue":"4","key":"19_CR2","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1016\/S0020-0190(98)00106-9","volume":"67","author":"F Baader","year":"1998","unstructured":"Baader, F.: On the complexity of Boolean unification. Inf. Process. Lett. 67(4), 215\u2013220 (1998)","journal-title":"Inf. Process. Lett."},{"issue":"3","key":"19_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-6(3:17)2010","volume":"6","author":"F Baader","year":"2010","unstructured":"Baader, F., Morawska, B.: Unification in the description logic $$\\cal{EL}$$ . Log. Methods Comput. Sci. 6(3), 1\u201331 (2010)","journal-title":"Log. Methods Comput. Sci."},{"key":"19_CR4","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1006\/jsco.2000.0426","volume":"31","author":"F Baader","year":"2001","unstructured":"Baader, F., Narendran, P.: Unification of concept terms in description logics. J. Symb. Comput. 31, 277\u2013305 (2001)","journal-title":"J. Symb. Comput."},{"issue":"1","key":"19_CR5","first-page":"97","volume":"4","author":"H Behmann","year":"1950","unstructured":"Behmann, H.: Das Aufl\u00f6sungsproblem in der Klassenlogik. Archiv f\u00fcr Philosophie 4(1), 97\u2013109 (1950). (First of two parts, also published in Archiv f\u00fcr mathematische Logik und Grundlagenforschung, 1.1 (1950), pp. 17\u201329)","journal-title":"Archiv f\u00fcr Philosophie"},{"issue":"2","key":"19_CR6","first-page":"193","volume":"4","author":"H Behmann","year":"1951","unstructured":"Behmann, H.: Das Aufl\u00f6sungsproblem in der Klassenlogik. Archiv f\u00fcr Philosophie 4(2), 193\u2013211 (1951). (Second of two parts, also published in Archiv f\u00fcr mathematische Logik und Grundlagenforschung, 1.2 (1951), pp. 33\u201351)","journal-title":"Archiv f\u00fcr Philosophie"},{"key":"19_CR7","volume-title":"Boolean Reasoning","author":"FM Brown","year":"2003","unstructured":"Brown, F.M.: Boolean Reasoning, 2nd edn. Dover Publications, Mineola (2003)","edition":"2"},{"issue":"2","key":"19_CR8","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/S0747-7171(87)80065-2","volume":"4","author":"W B\u00fcttner","year":"1987","unstructured":"B\u00fcttner, W., Simonis, H.: Embedding Boolean expressions into logic programming. J. Symb. Comput. 4(2), 191\u2013205 (1987)","journal-title":"J. Symb. Comput."},{"key":"19_CR9","unstructured":"Carlsson, M.: Boolean constraints in SICStus Prolog. Technical report SICS T91:09, Swedish Institute of Computer Science, Kista (1991)"},{"issue":"1:5","key":"19_CR10","first-page":"1","volume":"2","author":"W Conradie","year":"2006","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)","journal-title":"LMCS"},{"issue":"3","key":"19_CR11","doi-asserted-by":"crossref","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. J. Autom. Reason. 18(3), 297\u2013338 (1997)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"19_CR12","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1093\/logcom\/exv059","volume":"27","author":"S Eberhard","year":"2017","unstructured":"Eberhard, S., Hetzl, S., Weller, D.: Boolean unification with predicates. J. Log. Comput. 27(1), 109\u2013128 (2017)","journal-title":"J. Log. Comput."},{"key":"19_CR13","volume-title":"Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications","author":"DM Gabbay","year":"2008","unstructured":"Gabbay, D.M., Schmidt, R.A., Sza\u0142as, A.: Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. College Publications, London (2008)"},{"key":"19_CR14","unstructured":"Gabbay, D., Ohlbach, H.J.: Quantifier elimination in second-order predicate logic. In: KR 1992, pp. 425\u2013435. Morgan Kaufmann (1992)"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Kanellakis, P.C., Kuper, G.M., Revesz, P.Z.: Constraint query languages. In: PODS 1990, pp. 299\u2013313. ACM Press (1990)","DOI":"10.1145\/298514.298582"},{"issue":"1","key":"19_CR16","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1006\/jcss.1995.1051","volume":"51","author":"PC Kanellakis","year":"1995","unstructured":"Kanellakis, P.C., Kuper, G.M., Revesz, P.Z.: Constraint query languages. J. Comput. Syst. Sci. 51(1), 26\u201352 (1995)","journal-title":"J. Comput. Syst. Sci."},{"key":"19_CR17","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 $$\\cal{ALC}$$ -ontologies using fixpoints. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS, vol. 8152, pp. 87\u2013102. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-40885-4_7"},{"key":"19_CR18","unstructured":"L\u00f6wenheim, L.: \u00dcber das Aufl\u00f6sungsproblem im logischen Klassenkalk\u00fcl. In: Sitzungsberichte der Berliner Mathematischen Gesellschaft, vol. 7, pp. 89\u201394. Teubner (1908)"},{"key":"19_CR19","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/BF01474159","volume":"68","author":"L L\u00f6wenheim","year":"1910","unstructured":"L\u00f6wenheim, L.: \u00dcber die Aufl\u00f6sung von Gleichungen im logischen Gebietekalk\u00fcl. Math. Ann. 68, 169\u2013207 (1910)","journal-title":"Math. Ann."},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1007\/3-540-16780-3_115","volume-title":"8th International Conference on Automated Deduction","author":"U Martin","year":"1986","unstructured":"Martin, U., Nipkow, T.: Unification in Boolean rings. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 506\u2013513. Springer, Heidelberg (1986). doi: 10.1007\/3-540-16780-3_115"},{"issue":"4","key":"19_CR21","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/BF00297246","volume":"4","author":"U Martin","year":"1988","unstructured":"Martin, U., Nipkow, T.: Unification in Boolean rings. J. Autom. Reason. 4(4), 381\u2013396 (1988)","journal-title":"J. Autom. Reason."},{"key":"19_CR22","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1016\/S0747-7171(89)80013-6","volume":"7","author":"U Martin","year":"1989","unstructured":"Martin, U., Nipkow, T.: Boolean unification - the story so far. J. Symb. Comput. 7, 275\u2013293 (1989)","journal-title":"J. Symb. Comput."},{"key":"19_CR23","volume-title":"Boolean Functions and Equations","author":"S Rudeanu","year":"1974","unstructured":"Rudeanu, S.: Boolean Functions and Equations. Elsevier, Amsterdam (1974)"},{"key":"19_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0241-0","volume-title":"Lattice Functions and Equations","author":"S Rudeanu","year":"2001","unstructured":"Rudeanu, S.: Lattice Functions and Equations. Springer, London (2001). doi: 10.1007\/978-1-4471-0241-0"},{"key":"19_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-642-39799-8_24","volume-title":"Computer Aided Verification","author":"P R\u00fcmmer","year":"2013","unstructured":"R\u00fcmmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for Horn-clause verification. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 347\u2013363. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_24"},{"issue":"1","key":"19_CR26","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1016\/j.jal.2012.01.001","volume":"10","author":"RA Schmidt","year":"2012","unstructured":"Schmidt, R.A.: The Ackermann approach for modal logic, correspondence theory and second-order reduction. J. Appl. Log. 10(1), 52\u201374 (2012)","journal-title":"J. Appl. Log."},{"key":"19_CR27","unstructured":"Schr\u00f6der, E.: Vorlesungen \u00fcber die Algebra der Logik. Teubner (vol. 1, 1890; vol. 2, pt. 1, 1891; vol. 2, pt. 2, 1905; vol. 3, 1895)"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Seidl, M., Lonsing, F., Biere, A.: bf2epr: a tool for generating EPR formulas from QBF. In: PAAR-2012. EPiC, vol. 21, pp. 139\u2013148 (2012)","DOI":"10.29007\/2b5d"},{"key":"19_CR29","first-page":"181","volume":"37","author":"V Sofronie","year":"1989","unstructured":"Sofronie, V.: Formula-handling computer solution of Boolean equations. I. Ring equations. Bull. EATCS 37, 181\u2013186 (1989)","journal-title":"Bull. EATCS"},{"key":"19_CR30","doi-asserted-by":"crossref","unstructured":"Wernhard, C.: The Boolean solution problem from the perspective of predicate logic - extended version. Technical report KRR 17-01, TU Dresden (2017)","DOI":"10.1007\/978-3-319-66167-4_19"},{"key":"19_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"587","DOI":"10.1007\/978-3-319-25007-6_34","volume-title":"The Semantic Web - ISWC 2015","author":"Y Zhao","year":"2015","unstructured":"Zhao, Y., Schmidt, R.A.: Concept forgetting in $$\\cal{ALCOI}$$ -ontologies using an Ackermann approach. In: Arenas, M., et al. (eds.) ISWC 2015. LNCS, vol. 9366, pp. 587\u2013602. Springer, Cham (2015). doi: 10.1007\/978-3-319-25007-6_34"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66167-4_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T03:53:06Z","timestamp":1750823586000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66167-4_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661667","9783319661674"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66167-4_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}