{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T19:10:47Z","timestamp":1754161847377,"version":"3.41.2"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031999833","type":"print"},{"value":"9783031999840","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T00:00:00Z","timestamp":1753833600000},"content-version":"vor","delay-in-days":210,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Second-order quantifier-elimination is the problem of finding, given a formula with second-order quantifiers, a logically equivalent first-order formula. While such formulas are not computable in general, there are practical algorithms and subclasses with applications throughout computational logic. One of the most prominent algorithms for second-order quantifier elimination is the SCAN algorithm which is based on saturation theorem proving. In this paper we show how the SCAN algorithm on clause sets can be extended to solve a more general problem: namely, finding an instance of the second-order quantifiers that results in a logically equivalent first-order formula. In addition we provide a prototype implementation of the proposed method. This work paves the way for applying the SCAN algorithm to new problems in application domains such as modal correspondence theory, knowledge representation, and verification.<\/jats:p>","DOI":"10.1007\/978-3-031-99984-0_27","type":"book-chapter","created":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:49Z","timestamp":1753789669000},"page":"511-531","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Computing Witnesses Using the\u00a0SCAN Algorithm"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-3799-6393","authenticated-orcid":false,"given":"Fabian","family":"Achammer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6461-5982","authenticated-orcid":false,"given":"Stefan","family":"Hetzl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6673-3333","authenticated-orcid":false,"given":"Renate A.","family":"Schmidt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,7,30]]},"reference":[{"key":"27_CR1","unstructured":"Achammer, F., Hetzl, S., Schmidt, R.A.: Computing witnesses using the SCAN algorithm (Extended Preprint) (2025). Preprint at https:\/\/achammer.dev\/research\/cade2025-extended-preprint"},{"issue":"1","key":"27_CR2","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. 110(1), 390\u2013413 (1935). https:\/\/doi.org\/10.1007\/BF01448035","journal-title":"Math. Ann."},{"key":"27_CR3","unstructured":"Alassaf, R., Schmidt, R.A., Sattler, U.: Saturation-based uniform interpolation for multi-modal logics. In: Fern\u00e1ndez-Duque, D., Palmigiano, A., Pinchinat, S. (eds.) Advances in Modal Logic, vol. 14, pp. 37\u201358. College Publications, London (2022). http:\/\/www.aiml.net\/volumes\/volume14"},{"key":"27_CR4","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/BF01190829","volume":"5","author":"L Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput. 5, 193\u2013212 (1994). https:\/\/doi.org\/10.1007\/BF01190829","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"27_CR5","doi-asserted-by":"publisher","unstructured":"Baumgartner, P., Waldmann, U.: Hierarchic superposition revisited. In: Lutz, C., Sattler, U., Tinelli, C., Turhan, A., Wolter, F. (eds.) Description Logic, Theory Combination, and All That. LNCS, vol. 11560, pp. 15\u201356. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-22102-7_2","DOI":"10.1007\/978-3-030-22102-7_2"},{"key":"27_CR6","doi-asserted-by":"publisher","unstructured":"Behmann, H.: Das Aufl\u00f6sungsproblem in der Klassenlogik. Archiv f\u00fcr mathematische Logik und Grundlagenforschung 1(1), 17\u201329 (1950). https:\/\/doi.org\/10.1007\/BF01976313, first of two parts","DOI":"10.1007\/BF01976313"},{"key":"27_CR7","doi-asserted-by":"publisher","unstructured":"Behmann, H.: Das Aufl\u00f6sungsproblem in der Klassenlogik. Archiv f\u00fcr mathematische Logik und Grundlagenforschung 1(2), 33\u201351 (1951). https:\/\/doi.org\/10.1007\/BF01982011, second of two parts","DOI":"10.1007\/BF01982011"},{"key":"27_CR8","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K.L., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday. LNCS, vol. 9300, pp. 24\u201351. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2","DOI":"10.1007\/978-3-319-23534-9_2"},{"issue":"2","key":"27_CR9","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0898-1221(94)00217-9","volume":"29","author":"C Brink","year":"1995","unstructured":"Brink, C., Gabbay, D.M., Ohlbach, H.J.: Towards automating duality. Comput. Math. Appl. 29(2), 73\u201390 (1995)","journal-title":"Comput. Math. Appl."},{"key":"27_CR10","doi-asserted-by":"publisher","unstructured":"Chen, J., Alghamdi, G., Schmidt, R.A., Walther, D., Gao, Y.: Ontology extraction for large ontologies via modularity and forgetting. In: Kejriwal, M., Szekely, P.A., Troncy, R. (eds.) Proceedings of the 10th International Conference on Knowledge Capture (K-CAP 1919), pp. 45\u201352. ACM (2019).https:\/\/doi.org\/10.1145\/3360901.3364424","DOI":"10.1145\/3360901.3364424"},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"Conradie, W., Goranko, V., Vakarelov, D.: Algorithmic correspondence and completeness in modal logic: I. The core algorithm SQEMA. Logical Methods Comput. Sci. 2(1:5), 1\u201326 (2006)","DOI":"10.2168\/LMCS-2(1:5)2006"},{"key":"27_CR12","doi-asserted-by":"publisher","unstructured":"Conradie, W., Ghilardi, S., Palmigiano, A.: Unified correspondence. In: Baltag, A., Smets, S. (eds.) Johan van Benthem on Logic and Information Dynamics, pp. 933\u2013975. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-06025-5_36","DOI":"10.1007\/978-3-319-06025-5_36"},{"key":"27_CR13","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1613\/JAIR.5530","volume":"60","author":"JP Delgrande","year":"2017","unstructured":"Delgrande, J.P.: A knowledge level account of forgetting. J. Artif. Intell. Res. 60, 1165\u20131213 (2017). https:\/\/doi.org\/10.1613\/JAIR.5530","journal-title":"J. Artif. Intell. Res."},{"issue":"3","key":"27_CR14","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1023\/A:1005722130532","volume":"18","author":"P Doherty","year":"1997","unstructured":"Doherty, P., Lukaszewicz, W., Szalas, A.: Computing circumscription revisited: a reduction algorithm. J. Autom. Reason. 18(3), 297\u2013336 (1997). https:\/\/doi.org\/10.1023\/A:1005722130532","journal-title":"J. Autom. Reason."},{"issue":"1","key":"27_CR15","doi-asserted-by":"publisher","first-page":"23","DOI":"10.3233\/FI-1998-3612","volume":"36","author":"P Doherty","year":"1998","unstructured":"Doherty, P., \u0141ukaszewicz, W., Sza\u0142as, A.: General domain circumscription and its effective reductions. Fund. Inform. 36(1), 23\u201355 (1998). https:\/\/doi.org\/10.3233\/FI-1998-3612","journal-title":"Fund. Inform."},{"key":"27_CR16","unstructured":"Doherty, P., Lukaszewicz, W., Szalas, A.: Computing strongest necessary and weakest sufficient conditions of first-order formulas. In: Nebel, B. (ed.) Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI 2001), pp. 145\u2013154. Morgan Kaufmann (2001)"},{"key":"27_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-540-25929-9_16","volume-title":"Rough Sets and Current Trends in Computing","author":"P Doherty","year":"2004","unstructured":"Doherty, P., Sza\u0142as, A.: On the correspondence between approximations and similarity. In: Tsumoto, S., S\u0142owi\u0144ski, R., Komorowski, J., Grzyma\u0142a-Busse, J.W. (eds.) RSCTC 2004. LNCS (LNAI), vol. 3066, pp. 143\u2013152. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-25929-9_16"},{"issue":"1","key":"27_CR18","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1093\/logcom\/exv059","journal-title":"J. Log. Comput."},{"key":"27_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-319-40229-1_20","volume-title":"Automated Reasoning","author":"G Ebner","year":"2016","unstructured":"Ebner, G., Hetzl, S., Reis, G., Riener, M., Wolfsteiner, S., Zivota, S.: System description: GAPT 2.0. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 293\u2013301. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_20"},{"issue":"1","key":"27_CR20","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/S13218-018-0564-6","volume":"33","author":"T Eiter","year":"2019","unstructured":"Eiter, T., Kern-Isberner, G.: A brief survey on forgetting from a knowledge representation and reasoning perspective. K\u00fcnstliche Intell. 33(1), 9\u201333 (2019). https:\/\/doi.org\/10.1007\/S13218-018-0564-6","journal-title":"K\u00fcnstliche Intell."},{"key":"27_CR21","unstructured":"Engel, T.: Quantifier elimination in second-order predicate logic. Diplomarbeit, Fachbereich Informatik, Univ. des Saarlandes, Saarbr\u00fccken, Germany (1996)"},{"key":"27_CR22","doi-asserted-by":"publisher","unstructured":"F\u00e9r\u00e9e, H., van\u00a0der Giessen, I., van Gool, S., Shillito, I.: Mechanised uniform interpolation for modal logics K, GL, and ISL. In: Benzm\u00fcller, C., Heule, M.J.H., Schmidt, R.A. (eds.) Automated Reasoning (IJCAR 2024). LNCS, vol. 14740, pp. 43\u201360. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-63501-4_3","DOI":"10.1007\/978-3-031-63501-4_3"},{"key":"27_CR23","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/BF01060210","volume":"7","author":"D Gabbay","year":"1992","unstructured":"Gabbay, D., Ohlbach, H.J.: Quantifier elimination in second order predicate logic. S. Afr. Comput. J. 7, 35\u201343 (1992)","journal-title":"S. Afr. Comput. J."},{"key":"27_CR24","unstructured":"Gabbay, D.M., Schmidt, R.A., Sza\u0142as, A.: Second-Order Quantifier Elimination. College Publications (2008)"},{"issue":"1","key":"27_CR25","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1017\/S1471068421000570","volume":"23","author":"R Gon\u00e7alves","year":"2023","unstructured":"Gon\u00e7alves, R., Knorr, M., Leite, J.: Forgetting in answer set programming: a survey. Theory Pract. Log. Program. 23(1), 111\u2013156 (2023). https:\/\/doi.org\/10.1017\/S1471068421000570","journal-title":"Theory Pract. Log. Program."},{"key":"27_CR26","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. 3051, pp. 149\u2013162. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24771-5_13"},{"key":"27_CR27","doi-asserted-by":"publisher","unstructured":"Hetzl, S., Kloibhofer, J.: A fixed-point theorem for Horn formula equations. In: Hojjat, H., Kafle, B. (eds.) 8th Workshop on Horn Clauses for Verification and Synthesis (HCVS). Electronic Proceedings in Theoretical Computer Science, vol.\u00a0344, pp. 65\u201378. Open Publishing Association (2021). https:\/\/doi.org\/10.4204\/EPTCS.344.5","DOI":"10.4204\/EPTCS.344.5"},{"key":"27_CR28","unstructured":"Hetzl, S., Kloibhofer, J.: An abstract fixed-point theorem for Horn formula equations (Abstract). In: Schmidt, R.A., Wernhard, C., Zhao, Y. (eds.) Proceedings of the Second Workshop on Second-Order Quantifier Elimination and Related Topics (SOQE). CEUR Workshop Proceedings, vol.\u00a03009, pp. 59\u201360. CEUR-WS.org (2021)"},{"key":"27_CR29","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-14203-1_16","volume-title":"Automated Reasoning","author":"K Hoder","year":"2010","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Interpolation and symbol elimination in vampire. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 188\u2013195. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_16"},{"key":"27_CR30","unstructured":"Hodges, W.: A Shorter Model Theory. Cambridge University Press (1997)"},{"key":"27_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-319-40970-2_22","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"Z Khasidashvili","year":"2016","unstructured":"Khasidashvili, Z., Korovin, K.: Predicate elimination for preprocessing in first-order theorem proving. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 361\u2013372. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_22"},{"key":"27_CR32","unstructured":"Konev, B., Walther, D., Wolter, F.: Forgetting and uniform interpolation in large-scale description logic terminologies. In: Boutilier, C. (ed.) Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI 2009), pp. 830\u2013835 (2009). http:\/\/ijcai.org\/papers09\/Papers\/IJCAI09-142.pdf"},{"key":"27_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1007\/978-3-642-45221-5_37","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P Koopmann","year":"2013","unstructured":"Koopmann, P., Schmidt, R.A.: Forgetting concept and role symbols in $$\\cal{ALCH}$$-ontologies. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 552\u2013567. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-45221-5_37"},{"key":"27_CR34","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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 (LNAI), vol. 8152, pp. 87\u2013102. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40885-4_7"},{"key":"27_CR35","doi-asserted-by":"crossref","unstructured":"Koopmann, P., Schmidt, R.A.: Uniform interpolation and forgetting for $$\\cal{ALC}$$ ontologies with aboxes. In: Bonet, B., Koenig, S. (eds.) Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI-2015), pp. 175\u2013181. AAAI Press (2015)","DOI":"10.1609\/aaai.v29i1.9206"},{"key":"27_CR36","doi-asserted-by":"publisher","unstructured":"Koopmann, P., Del-Pinto, W., Tourret, S., Schmidt, R.A.: Signature-based abduction for expressive description logics. In: Calvanese, D., Erdem, E., Thielscher, M. (eds.) Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR 2020), pp. 592\u2013602. AI Press (2020). https:\/\/doi.org\/10.24963\/kr.2020\/59","DOI":"10.24963\/kr.2020\/59"},{"key":"27_CR37","unstructured":"Lin, F., Reiter, R.: Forget it!. In: Presented at the AAAI Fall Symposium on Relevance, New Orleans (1994)"},{"key":"27_CR38","doi-asserted-by":"publisher","unstructured":"Liu, Z., Lu, C., Alghamdi, G., Schmidt, R.A., Zhao, Y.: Tracking semantic evolutionary changes in large-scale ontological knowledge bases. In: Demartini, G., Zuccon, G., Culpepper, J.S., Huang, Z., Tong, H. (eds.) CIKM 2021: The 30th ACM International Conference on Information and Knowledge Management, pp. 1130\u20131139. ACM (2021). https:\/\/doi.org\/10.1145\/3459637.3482307","DOI":"10.1145\/3459637.3482307"},{"key":"27_CR39","unstructured":"Ludwig, M., Konev, B.: Practical uniform interpolation and forgetting for ALC tboxes with applications to logical difference. In: Baral, C., De Giacomo, G., Eiter, T. (eds.) Principles of Knowledge Representation and Reasoning (KR 2014). AAAI Press (2014)"},{"issue":"3\u20134","key":"27_CR40","doi-asserted-by":"publisher","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(3\u20134), 275\u2013293 (1989). https:\/\/doi.org\/10.1016\/S0747-7171(89)80013-6","journal-title":"J. Symb. Comput."},{"key":"27_CR41","unstructured":"Nonnengart, A., Sza\u0142as, A.: A fixpoint approach to second-order quantifier elimination with applications to correspondence theory. In: Or\u0142owska, E. (ed.) Logic at Work: Essays Dedicated to the Memory of Helena Rasiowa, Studies in Fuzziness and Soft Computing, vol.\u00a024, pp. 307\u2013328. Springer (1998)"},{"key":"27_CR42","unstructured":"Odersky, M., et al.: An overview of the Scala programming language (2004). https:\/\/infoscience.epfl.ch\/handle\/20.500.14299\/214698"},{"key":"27_CR43","doi-asserted-by":"publisher","unstructured":"Nonnengart, A., Ohlbach, H.J., Sza\u0142as, A.: Elimination of predicate quantifiers. In: Ohlbach, H.J., Reyle, U. (eds.) Logic, Language and Reasoning. Trends in Logic, vol. 5, pp. 149\u2013171. Springer, Dordrecht (1999). https:\/\/doi.org\/10.1007\/978-94-011-4574-9_9","DOI":"10.1007\/978-94-011-4574-9_9"},{"key":"27_CR44","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-030-86205-3_3","volume-title":"Frontiers of Combining Systems","author":"D Peuter","year":"2021","unstructured":"Peuter, D., Sofronie-Stokkermans, V.: Symbol elimination and applications to parametric entailment problems. In: Konev, B., Reger, G. (eds.) FroCoS 2021. LNCS (LNAI), vol. 12941, pp. 43\u201362. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86205-3_3"},{"key":"27_CR45","unstructured":"Rudeanu, S.: Boolean Functions and Equations. North-Holland (1974)"},{"key":"27_CR46","unstructured":"Schr\u00f6der, E.: Vorlesungen \u00fcber die Algebra der Logik, vol.\u00a01. Teubner (1890)"},{"key":"27_CR47","doi-asserted-by":"publisher","unstructured":"Toluhi, D., Schmidt, R.A., Parsia, B.: Concept description and definition extraction for the ANEMONE system. In: Alechina, N., Baldoni, M., Logan, B. (eds.) Engineering Multi-Agent Systems (EMAS 2021), Revised Selected Papers. LNCS, vol. 13190, pp. 352\u2013372. Springer (2021).https:\/\/doi.org\/10.1007\/978-3-030-97457-2_20","DOI":"10.1007\/978-3-030-97457-2_20"},{"key":"27_CR48","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-319-66167-4_19","volume-title":"Frontiers of Combining Systems","author":"C Wernhard","year":"2017","unstructured":"Wernhard, C.: The Boolean solution problem from the perspective of predicate logic. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 333\u2013350. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66167-4_19"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 30"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99984-0_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:53Z","timestamp":1753789673000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99984-0_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031999833","9783031999840"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99984-0_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"30 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Stuttgart","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.dhbw-stuttgart.de\/cade-30\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}