{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,12]],"date-time":"2026-11-12T16:46:52Z","timestamp":1794502012611,"version":"4.9.1"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319214009","type":"print"},{"value":"9783319214016","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","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":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_21","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T06:13:46Z","timestamp":1437718426000},"page":"311-325","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Quantifier-Free Equational Logic and Prime Implicate Generation"],"prefix":"10.1007","author":[{"given":"Mnacho","family":"Echenim","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nicolas","family":"Peltier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sophie","family":"Tourret","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"issue":"1","key":"21_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1459010.1459014","volume":"10","author":"A Armando","year":"2009","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1), 1\u201351 (2009)","journal-title":"ACM Trans. Comput. Log."},{"key":"21_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"21_CR3","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0. Technical report, Department of Computer Science, The University of Iowa (2010). www.SMT-LIB.org"},{"issue":"2","key":"21_CR4","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/j.jsc.2008.10.008","volume":"45","author":"MP Bonacina","year":"2010","unstructured":"Bonacina, M.P., Echenim, M.: Theory decision by decomposition. J. Symb. Comput. 45(2), 229\u2013260 (2010)","journal-title":"J. Symb. Comput."},{"key":"21_CR5","unstructured":"Cruanes, S.:. Logtk: A logic ToolKit for automated reasoning and its implementation. In: 4th Workshop on Practical Aspects of Automated Reasoning (2014)"},{"key":"21_CR6","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":"21_CR7","doi-asserted-by":"crossref","unstructured":"Dershowitz, N.: Orderings for term-rewriting systems. In: Proceedings of the 20th Annual Symposium on Foundations of Computer Science, pp. 123\u2013131. IEEE Computer Society, Washington (1979)","DOI":"10.1109\/SFCS.1979.32"},{"key":"21_CR8","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)"},{"key":"21_CR9","unstructured":"Echenim, M., Peltier, N., Tourret, S.: An approach to abductive reasoning in equational logic. In: Rossi, F. (ed.) IJCAI 2013 - International Joint Conference on Artificial Intelligence, pp. 531\u2013537. AAAI Press, Beijing, August 2013"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, Heidelberg (2014)"},{"key":"21_CR11","unstructured":"Iwanuma, K., Nabeshima, H., Inoue.: Toward an efficient equality computation in connection tableaux: A modification method without symmetry transformation\u2014a preliminary report . First-Order Theorem Proving, p. 19 (2009)"},{"key":"21_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - CADE-11","author":"P Jackson","year":"1992","unstructured":"Jackson, P.: Computing prime implicates incrementally. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607. Springer, Heidelberg (1992)"},{"issue":"2","key":"21_CR13","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":"21_CR14","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":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. Springer, Heidelberg (1991)"},{"key":"21_CR16","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)"},{"key":"21_CR17","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)"},{"issue":"1","key":"21_CR18","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"},{"issue":"2","key":"21_CR19","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":"21_CR20","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/B978-044450813-3\/50009-6","volume-title":"Handbook of Automated Reasoning","author":"R Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 371\u2013443. North Holland, Amsterdam (2001)"},{"key":"21_CR21","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0304-3975(88)90146-6","volume":"59","author":"M Schmidt-Schauss","year":"1988","unstructured":"Schmidt-Schauss, M.: Implication of clauses is undecidable. Theor. Comput. Sci. 59, 287\u2013296 (1988)","journal-title":"Theor. Comput. Sci."},{"issue":"2\u20133","key":"21_CR22","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E - a brainiac theorem prover. AI Commun. 15(2\u20133), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"21_CR23","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-19 2013. LNCS, vol. 8312, pp. 735\u2013743. Springer, Heidelberg (2013)"},{"key":"21_CR24","unstructured":"Simon, L., Del Val A.: Efficient consequence finding. In: International Joint Conference on Artificial Intelligence, vol. 17, pp. 359\u2013370. Lawrence Erlbaum Associates ltd (2001)"},{"issue":"4","key":"21_CR25","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure: The FOF and CNF parts, v3.5.0. J. Autom. Reason. 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reason."},{"issue":"4","key":"21_CR26","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1109\/PGEC.1967.264648","volume":"EC\u201316","author":"P Tison","year":"1967","unstructured":"Tison, P.: Generalization of consensus theory and application to the minimization of boolean functions. IEEE Trans. Electron. Comput. EC\u201316(4), 446\u2013456 (1967)","journal-title":"IEEE Trans. Electron. Comput."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T04:46:37Z","timestamp":1676954797000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_21","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}