{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T09:02:51Z","timestamp":1773478971344,"version":"3.50.1"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319942049","type":"print"},{"value":"9783319942056","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-94205-6_19","type":"book-chapter","created":{"date-parts":[[2018,6,29]],"date-time":"2018-06-29T16:22:50Z","timestamp":1530289370000},"page":"279-294","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["A Generic Framework for Implicate Generation Modulo Theories"],"prefix":"10.1007","author":[{"given":"Mnacho","family":"Echenim","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Peltier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yanis","family":"Sellami","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,6,30]]},"reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"19_CR2","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2010). www.SMT-LIB.org"},{"key":"19_CR3","unstructured":"Bienvenu, M.: Prime implicates and prime implicants in modal logic. In: Proceedings of the National Conference on Artificial Intelligence, vol. 22, p. 379. AAAI Press\/MIT Press, Menlo Park, Cambridge, London (1999, 2007)"},{"key":"19_CR4","series-title":"Studies in Logic and Practical Reasoning","volume-title":"Handbook of Modal Logic","author":"P Blackburn","year":"2007","unstructured":"Blackburn, P., Van Benthem, J., Wolter, F.: Handbook of Modal Logic. Studies in Logic and Practical Reasoning, vol. 3. Elsevier, Amsterdam (2007). ISSN 1570\u20132464"},{"key":"19_CR5","unstructured":"De Kleer, J.: An improved incremental algorithm for generating prime implicates. In: Proceedings of the National Conference on Artificial Intelligence, p. 780. Wiley (1992)"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/978-3-642-31424-7_30","volume-title":"Computer Aided Verification","author":"I Dillig","year":"2012","unstructured":"Dillig, I., Dillig, T., McMillan, K.L., Aiken, A.: Minimum satisfying assignments for SMT. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 394\u2013409. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_30"},{"issue":"2","key":"19_CR8","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s10817-015-9344-2","volume":"57","author":"M Echenim","year":"2016","unstructured":"Echenim, M., Peltier, N.: A superposition calculus for abductive reasoning. J. Autom. Reason. 57(2), 97\u2013134 (2016)","journal-title":"J. Autom. Reason."},{"key":"19_CR9","unstructured":"Echenim, M., Peltier, N., Tourret, S.: An approach to abductive reasoning in equational logic. In: Proceedings of International Conference on Artificial Intelligence, IJCAI 2013, pp. 3\u20139. AAAI (2013)"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-319-08587-6_10","volume-title":"Automated Reasoning","author":"M Echenim","year":"2014","unstructured":"Echenim, M., Peltier, N., Tourret, S.: A rewriting strategy to generate prime implicates in equational logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 137\u2013151. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_10"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-319-21401-6_21","volume-title":"Automated Deduction \u2013 CADE-25","author":"M Echenim","year":"2015","unstructured":"Echenim, M., Peltier, N., Tourret, S.: Quantifier-free equational logic and prime implicate generation. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 311\u2013325. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_21"},{"key":"19_CR12","doi-asserted-by":"crossref","first-page":"827","DOI":"10.1613\/jair.5481","volume":"60","author":"M Echenim","year":"2017","unstructured":"Echenim, M., Peltier, N., Tourret, S.: Prime implicate generation in equational logic. J. Artif. Intell. Res. 60, 827\u2013880 (2017)","journal-title":"J. Artif. Intell. Res."},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"issue":"9","key":"19_CR14","doi-asserted-by":"publisher","first-page":"490","DOI":"10.1145\/367390.367400","volume":"3","author":"E Fredkin","year":"1960","unstructured":"Fredkin, E.: Trie memory. Commun. ACM 3(9), 490\u2013499 (1960)","journal-title":"Commun. ACM"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-55602-8_170","volume-title":"Automated Deduction\u2014CADE 2011","author":"P Jackson","year":"1992","unstructured":"Jackson, P.: Computing prime implicates incrementally. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 253\u2013267. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_170"},{"issue":"2","key":"19_CR16","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/S0747-7171(08)80029-6","volume":"9","author":"A Kean","year":"1990","unstructured":"Kean, A., Tsiknis, G.: An incremental method for generating prime implicants\/implicates. J. Symb. Comput. 9(2), 185\u2013206 (1990)","journal-title":"J. Symb. Comput."},{"issue":"1","key":"19_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(93)90243-M","volume":"120","author":"E Knill","year":"1993","unstructured":"Knill, E., Cox, P.T., Pietrzykowski, T.: Equality and abductive residua for Horn clauses. Theoret. Comput. Sci. 120(1), 1\u201344 (1993)","journal-title":"Theoret. Comput. Sci."},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/3-540-54507-7_12","volume-title":"Fundamentals of Artificial Intelligence Research","author":"P Marquis","year":"1991","unstructured":"Marquis, P.: Extending abduction from propositional to first-order logic. In: Jorrand, P., Kelemen, J. (eds.) FAIR 1991. LNCS, vol. 535, pp. 141\u2013155. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-54507-7_12"},{"key":"19_CR19","series-title":"Handbook of Defeasible Reasoning and Uncertainty Management Systems","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-94-017-1737-3_3","volume-title":"Handbook of Defeasible Reasoning and Uncertainty Management Systems","author":"P Marquis","year":"2000","unstructured":"Marquis, P.: Consequence finding algorithms. In: Kohlas, J., Moral, S. (eds.) Handbook of Defeasible Reasoning and Uncertainty Management Systems. HAND, vol. 5, pp. 41\u2013145. Springer, Dordrecht (2000). https:\/\/doi.org\/10.1007\/978-94-017-1737-3_3"},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-642-02716-1_19","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"A Matusiewicz","year":"2009","unstructured":"Matusiewicz, A., Murray, N.V., Rosenthal, E.: Prime implicate tries. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol. 5607, pp. 250\u2013264. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02716-1_19"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-642-21916-0_23","volume-title":"Foundations of Intelligent Systems","author":"A Matusiewicz","year":"2011","unstructured":"Matusiewicz, A., Murray, N.V., Rosenthal, E.: Tri-based set operations and selective computation of prime implicates. In: Kryszkiewicz, M., Rybinski, H., Skowron, A., Ra\u015b, Z.W. (eds.) ISMIS 2011. LNCS, vol. 6804, pp. 203\u2013213. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21916-0_23"},{"issue":"1","key":"19_CR22","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1093\/jigpal\/1.1.99","volume":"1","author":"MC Mayer","year":"1993","unstructured":"Mayer, M.C., Pirri, F.: First order abduction via tableau and sequent calculi. Log. J. IGPL 1(1), 99\u2013117 (1993)","journal-title":"Log. J. IGPL"},{"key":"19_CR23","unstructured":"Mishchenko, A.: An introduction to zero-suppressed binary decision diagrams. Technical report, Proceedings of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (2001)"},{"issue":"2","key":"19_CR24","doi-asserted-by":"crossref","first-page":"183","DOI":"10.3233\/AIC-2010-0465","volume":"23","author":"H Nabeshima","year":"2010","unstructured":"Nabeshima, H., Iwanuma, K., Inoue, K., Ray, O.: SOLAR: an automated deduction system for consequence finding. AI Commun. 23(2), 183\u2013203 (2010)","journal-title":"AI Commun."},{"key":"19_CR25","unstructured":"Previti, A., Ignatiev, A., Morgado, A., Marques-Silva, J.: Prime compilation of non-clausal formulae. In: Proceedings of the 24th International Conference on Artificial Intelligence, pp. 1980\u20131987. AAAI Press (2015)"},{"issue":"9","key":"19_CR26","doi-asserted-by":"publisher","first-page":"627","DOI":"10.1080\/00029890.1955.11988710","volume":"62","author":"W Quine","year":"1955","unstructured":"Quine, W.: A way to simplify truth functions. Am. Math. Mon. 62(9), 627\u2013631 (1955)","journal-title":"Am. Math. Mon."},{"key":"19_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/3-540-45744-5_29","volume-title":"Automated Reasoning","author":"A Riazanov","year":"2001","unstructured":"Riazanov, A., Voronkov, A.: Vampire 1.1 (system description). In: Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 376\u2013380. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45744-5_29"},{"key":"19_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"735","DOI":"10.1007\/978-3-642-45221-5_49","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S Schulz","year":"2013","unstructured":"Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 735\u2013743. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-45221-5_49"},{"key":"19_CR29","unstructured":"Simon, L., Del Val, A.: Efficient consequence finding. In: Proceedings of the 17th International Joint Conference on Artificial Intelligence, pp. 359\u2013370 (2001)"},{"key":"19_CR30","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1109\/PGEC.1967.264648","volume":"4","author":"P Tison","year":"1967","unstructured":"Tison, P.: Generalization of consensus theory and application to the minimization of boolean functions. IEEE Trans. Electron. Comput. 4, 446\u2013456 (1967)","journal-title":"IEEE Trans. Electron. Comput."},{"key":"19_CR31","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-48660-7_34","volume-title":"Automated Deduction \u2014 CADE-16","author":"Christoph Weidenbach","year":"1999","unstructured":"Weidenbach, C., Afshordel, B., Brahm, U., Cohrs, C., Engel, T., Keen, E., Theobalt, C., Topi\u0107, D.: System description: Spass version 1.0.0. In: CADE 1999. LNCS, vol. 1632, pp. 378\u2013382. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48660-7_34"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94205-6_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,4]],"date-time":"2020-11-04T19:17:36Z","timestamp":1604517456000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94205-6_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319942049","9783319942056"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94205-6_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}