{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:48:44Z","timestamp":1725558524354},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642141270"},{"type":"electronic","value":"9783642141287"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14128-7_23","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T10:45:36Z","timestamp":1277808336000},"page":"263-277","source":"Crossref","is-referenced-by-count":3,"title":["Smart Matching"],"prefix":"10.1007","author":[{"given":"Andrea","family":"Asperti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrico","family":"Tassi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"23_CR1","series-title":"Systems and Implementation Techniques of Applied Logic Series","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/978-94-017-0435-9_4","volume-title":"Automated Deduction \u2014 A Basis for Applications","author":"W. Ahrendt","year":"1998","unstructured":"Ahrendt, W., Beckert, B., H\u00e4hnle, R., Menzel, W., Reif, W., Schellhorn, G., Schmitt, P.H.: Integrating automated and interactive theorem proving. In: Automated Deduction \u2014 A Basis for Applications. Systems and Implementation Techniques of Applied Logic Series, vol.\u00a0II(9), pp. 97\u2013116. Kluwer, Dordrecht (1998)"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/3-540-44802-0_36","volume-title":"Computer Science Logic","author":"A. Armando","year":"2001","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: Uniform derivation of decision procedures by superposition. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 513\u2013527. Springer, Heidelberg (2001)"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/978-3-642-03359-9_8","volume-title":"TPHOLs 2009","author":"A. Asperti","year":"2009","unstructured":"Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: Hints in unification. In: Urban, C. (ed.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 84\u201398. Springer, Heidelberg (2009)"},{"issue":"1","key":"23_CR4","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/s12046-009-0003-3","volume":"34","author":"A. Asperti","year":"2009","unstructured":"Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: A compact kernel for the Calculus of Inductive Constructions. Sadhana\u00a034(1), 71\u2013144 (2009)","journal-title":"Sadhana"},{"issue":"2","key":"23_CR5","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10817-007-9070-5","volume":"39","author":"A. Asperti","year":"2007","unstructured":"Asperti, A., Sacerdoti Coen, C., Tassi, E., Zacchiroli, S.: User interaction with the Matita proof assistant. Journal of Automated Reasoning\u00a039(2), 109\u2013139 (2007)","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-540-73086-6_14","volume-title":"Towards Mechanized Mathematical Assistants","author":"A. Asperti","year":"2007","unstructured":"Asperti, A., Tassi, E.: Higher order proof reconstruction from paramodulation-based refutations: The unit equality case. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM\/CALCULEMUS 2007. LNCS (LNAI), vol.\u00a04573, pp. 146\u2013160. Springer, Heidelberg (2007)"},{"issue":"3","key":"23_CR7","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput.\u00a04(3), 217\u2013247 (1994)","journal-title":"J. Log. Comput."},{"issue":"3-4","key":"23_CR8","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1023\/A:1021939521172","volume":"29","author":"M. Bezem","year":"2002","unstructured":"Bezem, M., Hendriks, D., de Nivelle, H.: Automated proof construction in type theory using resolution. J. Autom. Reasoning\u00a029(3-4), 253\u2013275 (2002)","journal-title":"J. Autom. Reasoning"},{"key":"23_CR9","unstructured":"The Coq proof-assistant (2009), http:\/\/coq.inria.fr"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Degtyarev, A., Voronkov, A.: Equality reasoning in sequent-based calculi. In: Handbook of Automated Reasoning, pp. 611\u2013706. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50012-6"},{"key":"23_CR11","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N.: Orderings for term-rewriting systems. Theor. Comput. Sci.\u00a017, 279\u2013301 (1982)","journal-title":"Theor. Comput. Sci."},{"key":"23_CR12","unstructured":"Dershowitz, N., Hsiang, J., Josephson, N.A., Plaisted, D.A.: Associative-commutative rewriting. In: IJCAI, pp. 940\u2013944 (1983)"},{"issue":"2","key":"23_CR13","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1023\/B:JARS.0000029963.64213.ac","volume":"32","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Nieuwenhuis, R., Nivela, P.: Fast term indexing with coded context trees. J. Autom. Reasoning\u00a032(2), 103\u2013120 (2004)","journal-title":"J. Autom. Reasoning"},{"key":"23_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/3-540-59200-8_52","volume-title":"Rewriting Techniques and Applications","author":"P. Graf","year":"1995","unstructured":"Graf, P.: Substitution tree indexing. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol.\u00a0914, pp. 117\u2013131. Springer, Heidelberg (1995)"},{"key":"23_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-48256-3_21","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Hurd","year":"1999","unstructured":"Hurd, J.: Integrating gandalf and hol. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 311\u2013322. Springer, Heidelberg (1999)"},{"key":"23_CR16","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. Technical Report NASA\/CP-2003-212448, Nasa technical reports (2003)"},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational problems in Abstract Algebra, pp. 263\u2013297 (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"issue":"2","key":"23_CR18","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"W. McCune","year":"1992","unstructured":"McCune, W.: Experiments with discrimination tree indexing and path indexing for term retrieval. Journal of Automated Reasoning\u00a09(2), 147\u2013167 (1992)","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"23_CR19","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/s10817-007-9085-y","volume":"40","author":"J. Meng","year":"2008","unstructured":"Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reasoning\u00a040(1), 35\u201360 (2008)","journal-title":"J. Autom. Reasoning"},{"issue":"10","key":"23_CR20","doi-asserted-by":"publisher","first-page":"1575","DOI":"10.1016\/j.ic.2005.05.010","volume":"204","author":"J. Meng","year":"2006","unstructured":"Meng, J., Quigley, C., Paulson, L.C.: Automation for interactive proof: First prototype. Inf. Comput.\u00a0204(10), 1575\u20131596 (2006)","journal-title":"Inf. Comput."},{"issue":"2","key":"23_CR21","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM\u00a027(2), 356\u2013364 (1980)","journal-title":"J. ACM"},{"key":"23_CR22","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based thorem proving. In: Handbook of Automated Reasoning, pp. 443\u2013471. Elsevier\/MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"issue":"3","key":"23_CR23","first-page":"73","volume":"5","author":"L.C. Paulson","year":"1999","unstructured":"Paulson, L.C.: A generic tableau prover and its integration with isabelle. J. UCS\u00a05(3), 73\u201387 (1999)","journal-title":"J. UCS"},{"issue":"2-3","key":"23_CR24","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of vampire. AI Communications\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Communications"},{"issue":"1-2","key":"23_CR25","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0747-7171(03)00040-3","volume":"36","author":"A. Riazanov","year":"2003","unstructured":"Riazanov, A., Voronkov, A.: Limited resource strategy in resolution theorem proving. J. Symb. Comput.\u00a036(1-2), 101\u2013115 (2003)","journal-title":"J. Symb. Comput."},{"key":"23_CR26","first-page":"51","volume":"1","author":"C. Sacerdoti Coen","year":"2008","unstructured":"Sacerdoti Coen, C., Tassi, E.: A constructive and formal proof of Lebesgue\u2019s dominated convergence theorem in the interactive theorem prover Matita. Journal of Formalized Reasoning\u00a01, 51\u201389 (2008)","journal-title":"Journal of Formalized Reasoning"},{"issue":"1","key":"23_CR27","first-page":"41","volume":"2","author":"M. Sozeau","year":"2009","unstructured":"Sozeau, M.: A new look at generalized rewriting in type theory. Journal of Formalized Reasoning\u00a02(1), 41\u201362 (2009)","journal-title":"Journal of Formalized Reasoning"},{"issue":"1","key":"23_CR28","doi-asserted-by":"crossref","first-page":"59","DOI":"10.3233\/AIC-2009-0441","volume":"22","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The 4th ijcar automated theorem proving system competition - casc-j4. AI Commun.\u00a022(1), 59\u201372 (2009)","journal-title":"AI Commun."},{"issue":"4","key":"23_CR29","doi-asserted-by":"publisher","first-page":"698","DOI":"10.1145\/321420.321429","volume":"14","author":"L. Wos","year":"1967","unstructured":"Wos, L., Robinson, G.A., Carson, D.F., Shalla, L.: The concept of demodulation in theorem proving. J. ACM\u00a014(4), 698\u2013709 (1967)","journal-title":"J. ACM"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14128-7_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:47:51Z","timestamp":1606186071000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14128-7_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642141270","9783642141287"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14128-7_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}