{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T04:04:50Z","timestamp":1746072290523,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":56,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642376504"},{"type":"electronic","value":"9783642376511"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"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":[[2013]]},"DOI":"10.1007\/978-3-642-37651-1_7","type":"book-chapter","created":{"date-parts":[[2013,4,5]],"date-time":"2013-04-05T04:10:01Z","timestamp":1365135001000},"page":"169-193","source":"Crossref","is-referenced-by-count":5,"title":["From Search to Computation: Redundancy Criteria and Simplification at Work"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Hillenbrand","sequence":"first","affiliation":[]},{"given":"Ruzica","family":"Piskac","sequence":"additional","affiliation":[]},{"given":"Uwe","family":"Waldmann","sequence":"additional","affiliation":[]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/3-540-45653-8_21","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"B. Afshordel","year":"2001","unstructured":"Afshordel, B., Hillenbrand, T., Weidenbach, C.: First-Order Atom Definitions Extended. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 309\u2013319. Springer, Heidelberg (2001)"},{"key":"7_CR2","doi-asserted-by":"publisher","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, New York (1998)"},{"key":"7_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-7118-2","volume-title":"Canonical Equational Proofs","author":"L. Bachmair","year":"1991","unstructured":"Bachmair, L.: Canonical Equational Proofs. Birkh\u00e4user, Boston (1991)"},{"key":"7_CR4","first-page":"346","volume-title":"[First Annual] Symposium on Logic in Computer Science","author":"L. Bachmair","year":"1986","unstructured":"Bachmair, L., Dershowitz, N., Hsiang, J.: Orderings for equational proofs. In: [First Annual] Symposium on Logic in Computer Science, June\u00a016\u201318, pp. 346\u2013357. IEEE Computer Society Press, Cambridge (1986)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-54317-1_89","volume-title":"Conditional and Typed Rewriting Systems","author":"L. Bachmair","year":"1991","unstructured":"Bachmair, L., Ganzinger, H.: Completion of First-Order Clauses with Equality by Strict Superposition (extended abstract). In: Okada, M., Kaplan, S. (eds.) CTRS 1990. LNCS, vol.\u00a0516, pp. 162\u2013180. Springer, Heidelberg (1991)"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/3-540-52885-7_105","volume-title":"10th International Conference on Automated Deduction","author":"L. Bachmair","year":"1990","unstructured":"Bachmair, L., Ganzinger, H.: On Restrictions of Ordered Paramodulation with Simplification. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, pp. 427\u2013441. Springer, Heidelberg (1990)"},{"issue":"3","key":"7_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. Journal of Logic and Computation\u00a04(3), 217\u2013247 (1994)","journal-title":"Journal of Logic and Computation"},{"issue":"6","key":"7_CR8","doi-asserted-by":"publisher","first-page":"1007","DOI":"10.1145\/293347.293352","volume":"45","author":"L. Bachmair","year":"1998","unstructured":"Bachmair, L., Ganzinger, H.: Ordered chaining calculi for first-order theories of transitive relations. Journal of the ACM\u00a045(6), 1007\u20131049 (1998)","journal-title":"Journal of the ACM"},{"doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a01, ch.\u00a02, pp. 19\u201399. Elsevier (2001)","key":"7_CR9","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60381-6_3","volume-title":"Conditional and Typed Rewriting Systems","author":"P. Balbiani","year":"1995","unstructured":"Balbiani, P.: Equation Solving in Geometrical Theories. In: Lindenstrauss, N., Dershowitz, N. (eds.) CTRS 1994. LNCS, vol.\u00a0968, Springer, Heidelberg (1995)"},{"key":"7_CR11","first-page":"179","volume":"11","author":"P. Balbiani","year":"1997","unstructured":"Balbiani, P.: M\u00e9canisation de la g\u00e9om\u00e9trie: incidence et orthogonalit\u00e9. Revue d\u2019Intelligence Artificielle\u00a011, 179\u2013211 (1997)","journal-title":"Revue d\u2019Intelligence Artificielle"},{"issue":"1","key":"7_CR12","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1145\/363647.363681","volume":"48","author":"D. Basin","year":"2001","unstructured":"Basin, D., Ganzinger, H.: Automated complexity analysis based on ordered resolution. Journal of the ACM\u00a048(1), 70\u2013109 (2001)","journal-title":"Journal of the ACM"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-19027-9_27","volume-title":"ESOP \u201988","author":"H. Bertling","year":"1988","unstructured":"Bertling, H., Ganzinger, H., Sch\u00e4fers, R.: CEC: A System for the Completion of Conditional Equational Specifications. In: Ganzinger, H. (ed.) ESOP 1988. LNCS, vol.\u00a0300, pp. 378\u2013379. Springer, Heidelberg (1988)"},{"unstructured":"Brinker, C.: Geometrisches Schlie\u00dfen mit SPASS. Diplomarbeit, Universit\u00e4t des Saarlandes and Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany (2000); Supervisors: Ganzinger, H., Weidenbach, C.","key":"7_CR14"},{"issue":"5","key":"7_CR15","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N.G. Bruijn de","year":"1972","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church\u2013Rosser theorem. Indagationes Mathematicae\u00a034(5), 381\u2013392 (1972)","journal-title":"Indagationes Mathematicae"},{"key":"7_CR16","doi-asserted-by":"publisher","first-page":"345","DOI":"10.2307\/2371045","volume":"58","author":"A. Church","year":"1936","unstructured":"Church, A.: An unsolvable problem of elementary number theory. American Journal of Mathematics\u00a058, 345\u2013363 (1936)","journal-title":"American Journal of Mathematics"},{"issue":"4","key":"7_CR17","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"P.J. Downey","year":"1980","unstructured":"Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. Journal of the ACM\u00a027(4), 758\u2013771 (1980)","journal-title":"Journal of the ACM"},{"key":"7_CR18","first-page":"161","volume-title":"Fourth Workshop on Automated Deduction","author":"M. Fay","year":"1979","unstructured":"Fay, M.: First-order unification in an equational theory. In: Fourth Workshop on Automated Deduction, pp. 161\u2013167. Academic Press, Austin (1979)"},{"unstructured":"Finkler, U., Mehlhorn, K.: Checking priority queues. In: Proceedings of the 10th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA 1999). Society for Industrial and Applied Mathematics, pp. 901\u2013902 (1999)","key":"7_CR19"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-19242-5_6","volume-title":"Conditional Term Rewriting Systems","author":"H. Ganzinger","year":"1988","unstructured":"Ganzinger, H.: A Completion Procedure for Conditional Equations. In: Kaplan, S., Jouannaud, J.-P. (eds.) CTRS 1987. LNCS, vol.\u00a0308, pp. 62\u201383. Springer, Heidelberg (1988)"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/3-540-50325-0_4","volume-title":"Recent Trends in Data Type Specification","author":"H. Ganzinger","year":"1988","unstructured":"Ganzinger, H.: Completion with History-Dependent Complexities for Generated Equations. In: Sannella, D., Tarlecki, A. (eds.) Abstract Data Types 1987. LNCS, vol.\u00a0332, pp. 73\u201391. Springer, Heidelberg (1988)"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/BFb0039613","volume-title":"STACS 87","author":"H. Ganzinger","year":"1987","unstructured":"Ganzinger, H.: Ground Term Confluence in Parametric Conditional Equational Specifications. In: Brandenburg, F.J., Vidal-Naquet, G., Wirsing, M. (eds.) STACS 1987. LNCS, vol.\u00a0247, pp. 286\u2013298. Springer, Heidelberg (1987)"},{"key":"7_CR23","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/S0747-7171(08)80132-0","volume":"11","author":"H. Ganzinger","year":"1991","unstructured":"Ganzinger, H.: A completion procedure for conditional equations. Journal of Symbolic Computation\u00a011, 51\u201381 (1991)","journal-title":"Journal of Symbolic Computation"},{"key":"7_CR24","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(90)90105-Q","volume":"89","author":"H. Ganzinger","year":"1991","unstructured":"Ganzinger, H.: Order-sorted completion: the many-sorted way. Theoretical Computer Science\u00a089, 3\u201332 (1991)","journal-title":"Theoretical Computer Science"},{"key":"7_CR25","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/3-540-63104-6_32","volume-title":"Automated Deduction - CADE-14","author":"H. Ganzinger","year":"1997","unstructured":"Ganzinger, H., Meyer, C., Weidenbach, C.: Soft Typing for Ordered Resolution. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol.\u00a01249, pp. 321\u2013335. Springer, Heidelberg (1997)"},{"unstructured":"Ganzinger, H., Nieuwenhuis, R., Nivela, P.: The Saturate system (1994), http:\/\/www.mpi-sb.mpg.de\/SATURATE","key":"7_CR26"},{"key":"7_CR27","first-page":"150","volume-title":"12th International Conference on Software Engineering","author":"H. Ganzinger","year":"1990","unstructured":"Ganzinger, H., Sch\u00e4fers, R.: System support for modular order-sorted horn clause specifications. In: 12th International Conference on Software Engineering, pp. 150\u2013159. IEEE Computer Society Press, Nice (1990)"},{"key":"7_CR28","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.ic.2004.10.010","volume":"199","author":"H. Ganzinger","year":"2005","unstructured":"Ganzinger, H., Stuber, J.: Superposition with equivalence reasoning and delayed clause normal form transformation. Information and Computation\u00a0199, 3\u201323 (2005)","journal-title":"Information and Computation"},{"unstructured":"Giegerich, R.: Specification and correctness of code generators \u2013 an experiment with the CEC-system. In: M\u00fcller, J., Ganzinger, H. (eds.) 1st German Workshop \u201cTerm Rewriting: Theory and Applications\u201d, SEKI-Report 89\/02. Universit\u00e4t Kaiserslautern (1989)","key":"7_CR29"},{"issue":"2&3","key":"7_CR30","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/0304-3975(90)90034-F","volume":"72","author":"I. Gnaedig","year":"1990","unstructured":"Gnaedig, I., Kirchner, C., Kirchner, H.: Equational completion in order-sorted algebras. Theoretical Computer Science\u00a072(2&3), 169\u2013202 (1990)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"7_CR31","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J. Hsiang","year":"1991","unstructured":"Hsiang, J., Rusinowitch, M.: Proving refutational completeness of theorem-proving strategies: The transfinite semantic tree method. Journal of the ACM\u00a038(3), 559\u2013587 (1991)","journal-title":"Journal of the ACM"},{"key":"7_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/BFb0052362","volume-title":"Rewriting Techniques and Applications","author":"F. Jacquemard","year":"1998","unstructured":"Jacquemard, F., Meyer, C., Weidenbach, C.: Unification in Extensions of Shallow Equational Theories. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol.\u00a01379, pp. 76\u201390. Springer, Heidelberg (1998)"},{"key":"7_CR33","doi-asserted-by":"publisher","first-page":"153","DOI":"10.2307\/2372027","volume":"57","author":"S. Kleene","year":"1935","unstructured":"Kleene, S.: A theory of positive integers in formal logic. American Journal of Mathematics\u00a057, 153\u2013173, 219\u2013244 (1935)","journal-title":"American Journal of Mathematics"},{"unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press, Oxford (1970); Reprinted in Siekmann and Wrightson [50], pp. 342\u2013376","key":"7_CR34"},{"issue":"2","key":"7_CR35","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1145\/151261.151265","volume":"40","author":"D.A. McAllester","year":"1993","unstructured":"McAllester, D.A.: Automatic recognition of tractability in inference relation. Journal of the ACM\u00a040(2), 284\u2013303 (1993)","journal-title":"Journal of the ACM"},{"unstructured":"Nieuwenhuis, R.: First-order completion techniques. Technical report, UPC-LSI, Cited in Nieuwenhuis and Rubio [38] (1991)","key":"7_CR36"},{"doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R.: Basic paramodulation and decidable theories (extended abstract). In: Proceedings 11th IEEE Symposium on Logic in Computer Science (LICS 1996), pp. 473\u2013482. IEEE Computer Society Press (1996)","key":"7_CR37","DOI":"10.1109\/LICS.1996.561464"},{"key":"7_CR38","series-title":"Lecture Notes in Computer Science","volume-title":"ESOP \u201992","author":"R. Nieuwenhuis","year":"1992","unstructured":"Nieuwenhuis, R., Rubio, A.: Basic Superposition is Complete. In: Krieg-Br\u00fcckner, B. (ed.) ESOP 1992. LNCS, vol.\u00a0582, Springer, Heidelberg (1992)"},{"key":"7_CR39","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1023\/A:1006496715975","volume":"26","author":"T. Nipkow","year":"2001","unstructured":"Nipkow, T.: More Church\u2013Rosser proofs (in Isabelle\/HOL). Journal of Automated Reasoning\u00a026, 51\u201366 (2001)","journal-title":"Journal of Automated Reasoning"},{"key":"7_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"7_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/3-540-56868-9_33","volume-title":"Rewriting Techniques and Applications","author":"P. Nivela","year":"1993","unstructured":"Nivela, P., Nieuwenhuis, R.: Saturation of First-Order (constrained) Clauses with the Saturate System. In: Kirchner, C. (ed.) RTA 1993. LNCS, vol.\u00a0690, pp. 436\u2013440. Springer, Heidelberg (1993)"},{"key":"7_CR42","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1109\/SEFM.2005.54","volume-title":"Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005)","author":"H. Nivelle de","year":"2005","unstructured":"de Nivelle, H., Piskac, R.: Verification of an off-line checker for priority queues. In: Aichernig, B.K., Beckert, B. (eds.) Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), pp. 210\u2013219. IEEE, Koblenz (2005)"},{"issue":"1","key":"7_CR43","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1093\/jigpal\/1.1.69","volume":"1","author":"H.J. Ohlbach","year":"1993","unstructured":"Ohlbach, H.J.: Translation methods for non-classical logics \u2013 an overview. Bulletin of the IGPL\u00a01(1), 69\u201390 (1993)","journal-title":"Bulletin of the IGPL"},{"issue":"1","key":"7_CR44","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"G.E. Peterson","year":"1983","unstructured":"Peterson, G.E.: A technique for establishing completeness results in theorem proving with equality. SIAM Journal on Computing\u00a012(1), 82\u2013100 (1983)","journal-title":"SIAM Journal on Computing"},{"unstructured":"Piskac, R.: Formal correctness of result checking for priority queues. Master\u2019s thesis, Universit\u00e4t des Saarlandes (February 2005)","key":"7_CR45"},{"issue":"2-3","key":"7_CR46","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"},{"unstructured":"Robinson, G., Wos, L.: Paramodulation and theorem-proving in first-order theories with equality. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol.\u00a04, ch.\u00a08, pp. 298\u2013313. Edinburgh University Press, Edinburgh (1969); Reprinted in Siekmann and Wrightson [50], pp. 298\u2013313","key":"7_CR47"},{"issue":"1&2","key":"7_CR48","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/S0747-7171(08)80131-9","volume":"11","author":"M. Rusinowitch","year":"1991","unstructured":"Rusinowitch, M.: Theorem-proving with resolution and superposition. Journal of Symbolic Computation\u00a011(1&2), 21\u201349 (January\/February 1991)","journal-title":"Journal of Symbolic Computation"},{"issue":"2\/3","key":"7_CR49","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E \u2013 A Brainiac Theorem Prover. Journal of AI Communications\u00a015(2\/3), 111\u2013126 (2002)","journal-title":"Journal of AI Communications"},{"key":"7_CR50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-81955-1","volume-title":"Automation of Reasoning: Classical Papers on Computational Logic 1967-1970","author":"J. Siekmann","year":"1983","unstructured":"Siekmann, J., Wrightson, G.: Automation of Reasoning: Classical Papers on Computational Logic 1967-1970, vol.\u00a02. Springer, Berlin (1983)"},{"issue":"1","key":"7_CR51","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1006\/inco.1995.1057","volume":"118","author":"M. Takahashi","year":"1995","unstructured":"Takahashi, M.: Parallel reductions in \u03bb-calculus. Information and Computation\u00a0118(1), 120\u2013127 (1995)","journal-title":"Information and Computation"},{"issue":"6","key":"7_CR52","doi-asserted-by":"publisher","first-page":"826","DOI":"10.1145\/268999.269003","volume":"44","author":"H. Wasserman","year":"1997","unstructured":"Wasserman, H., Blum, M.: Software reliability via run-time result-checking. Journal of the ACM\u00a044(6), 826\u2013849 (1997)","journal-title":"Journal of the ACM"},{"key":"7_CR53","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/3-540-48660-7_29","volume-title":"Automated Deduction - CADE-16","author":"C. Weidenbach","year":"1999","unstructured":"Weidenbach, C.: Towards an Automatic Analysis of Security Protocols in First-Order Logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 314\u2013328. Springer, Heidelberg (1999)"},{"key":"7_CR54","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/3-540-45620-1_22","volume-title":"Automated Deduction - CADE-18","author":"C. Weidenbach","year":"2002","unstructured":"Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobald, C., Topic, D.: SPASS Version 2.0. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 275\u2013277. Springer, Heidelberg (2002)"},{"key":"7_CR55","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/3-540-61511-3_75","volume-title":"Automated Deduction - Cade-13","author":"C. Weidenbach","year":"1996","unstructured":"Weidenbach, C., Gaede, B., Rock, G.: SPASS & FLOTTER, version 0.42. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol.\u00a01104, pp. 141\u2013145. Springer, Heidelberg (1996)"},{"key":"7_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0012820","volume-title":"9th International Conference on Automated Deduction","author":"H. Zhang","year":"1988","unstructured":"Zhang, H., Kapur, D.: First-Order Theorem Proving using Conditional Rewrite Rules. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol.\u00a0310, pp. 1\u201320. Springer, Heidelberg (1988)"}],"container-title":["Lecture Notes in Computer Science","Programming Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-37651-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T03:17:31Z","timestamp":1745983051000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-37651-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642376504","9783642376511"],"references-count":56,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-37651-1_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}