{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T04:04:51Z","timestamp":1746072291234,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":137,"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_1","type":"book-chapter","created":{"date-parts":[[2013,4,5]],"date-time":"2013-04-05T04:10:01Z","timestamp":1365135001000},"page":"1-18","source":"Crossref","is-referenced-by-count":0,"title":["Harald Ganzinger\u2019s Legacy: Contributions to Logics and Programming"],"prefix":"10.1007","author":[{"given":"Deepak","family":"Kapur","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Nieuwenhuis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reinhard","family":"Wilhelm","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"1_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 Transactions on Computational Logic\u00a010(1), 1\u201347 (2009)","journal-title":"ACM Transactions on Computational Logic"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-04222-5_5","volume-title":"Frontiers of Combining Systems","author":"E. Althaus","year":"2009","unstructured":"Althaus, E., Kruglov, E., Weidenbach, C.: Superposition Modulo Linear Arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol.\u00a05749, pp. 84\u201399. Springer, Heidelberg (2009)"},{"issue":"2","key":"1_CR3","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A. Armando","year":"2003","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Information and Computation\u00a0183(2), 140\u2013164 (2003)","journal-title":"Information and Computation"},{"issue":"1","key":"1_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0747-7171(88)80018-X","volume":"6","author":"L. Bachmair","year":"1988","unstructured":"Bachmair, L., Dershowitz, N.: Critical pair criteria for completion. Journal of Symbolic Computation\u00a06(1), 1\u201318 (1988)","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Bertling, H., Ganzinger, H.: Completion-time optimization of rewrite-time goal solving. In: Extended Abstracts of the Third International Workshop on Unification (Preliminary Version) (1989)","DOI":"10.1007\/3-540-51081-8_99"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Completion of first-order clauses with equality by strict superposition (abstract). In: Term Rewriting: Theory and Applications (Ext.\u00a0Abstracts of the 2nd German Workshop) (1990)","DOI":"10.1007\/3-540-54317-1_89"},{"key":"1_CR7","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":"1_CR8","series-title":"LNAI","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 (LNAI), vol.\u00a0449, pp. 427\u2013441. Springer, Heidelberg (1990)"},{"key":"1_CR9","unstructured":"Bachmair, L., Ganzinger, H.: Perfect model semantics for logic programs with equality. In: Furukawa, K. (ed.) Proceedings of the Eighth International Conference on Logic Programming, Paris, France, June 24-28, pp. 645\u2013659. The MIT Press (1991)"},{"key":"1_CR10","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. Technical Report MPI-I-91-208, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken (August 1991)"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/BFb0013068","volume-title":"Logic Programming and Automated Reasoning","author":"L. Bachmair","year":"1992","unstructured":"Bachmair, L., Ganzinger, H.: Non-clausal Resolution and Superposition with Selection and Redundancy Criteria. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, pp. 273\u2013284. Springer, Heidelberg (1992)"},{"key":"1_CR12","unstructured":"Bachmair, L., Ganzinger, H.: Associative-commutative superposition. Technical Report MPI-I-93-267, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken (December 1993)"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-60381-6_1","volume-title":"Conditional and Typed Rewriting Systems","author":"L. Bachmair","year":"1995","unstructured":"Bachmair, L., Ganzinger, H.: Associative-commutative Superposition. In: Lindenstrauss, N., Dershowitz, N. (eds.) CTRS 1994. LNCS, vol.\u00a0968, pp. 155\u2013167. Springer, Heidelberg (1995)"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/BFb0016860","volume-title":"Constraints in Computational Logics","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Buchberger\u2019s Algorithm: A Constraint-based Completion Procedure. In: Jouannaud, J.-P. (ed.) CCL 1994. LNCS, vol.\u00a0845, pp. 285\u2013301. Springer, Heidelberg (1994)"},{"key":"1_CR15","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/3-540-58156-1_32","volume-title":"Automated Deduction - CADE-12","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Ordered Chaining for Total Orderings. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol.\u00a0814, pp. 435\u2013450. Springer, Heidelberg (1994)"},{"issue":"3","key":"1_CR16","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"},{"key":"1_CR17","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite techniques for transitive relations. In: Ninth Annual IEEE Symposium on Logic in Computer Science, Paris, France (July 1994)"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Basin, D., Ganzinger, H.: Complexity Analysis Based on Ordered Resolution. In: Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press, New Brunswick, New Jersey, USA, pp. 456\u2013465. IEEE Computer Society Press (1996)","DOI":"10.1109\/LICS.1996.561462"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Ordered chaining calculi for first-order theories of transitive relations. Journal of the ACM\u00a045(6) (November 1998); Revised Version of MPI-I-95-2-00","DOI":"10.1145\/293347.293352"},{"key":"1_CR20","unstructured":"Bachmair, L., Ganzinger, H.: Equational reasoning in saturation-based theorem proving. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction: A Basis for Applications. Kluwer (1998)"},{"key":"1_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/BFb0054258","volume-title":"Automated Deduction - CADE-15","author":"L. Bachmair","year":"1998","unstructured":"Bachmair, L., Ganzinger, H.: Strict Basic Superposition. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 160\u2013174. Springer, Heidelberg (1998)"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, ch. 2, pp. 19\u201399. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"issue":"1","key":"1_CR23","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1145\/363647.363681","volume":"48","author":"D.A. Basin","year":"2001","unstructured":"Basin, D.A., 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":"1_CR24","doi-asserted-by":"crossref","unstructured":"Bertling, H., Ganzinger, H., Baumeister, H.: CEC (Conditional Equations Completion). In: Brandenburg, F.J., Vidal-Naquet, G., Wirsing, M. (eds.) STACS 1987. LNCS, vol.\u00a0247, p. 470. Springer, Heidelberg (1987)","DOI":"10.1007\/BFb0039629"},{"key":"1_CR25","series-title":"LNAI","first-page":"462","volume-title":"Automated Deduction - CADE-11","author":"L. Bachmair","year":"1992","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic Paramodulation and Superposition. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol.\u00a0607, pp. 462\u2013476. Springer, Heidelberg (1992)"},{"issue":"2","key":"1_CR26","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1006\/inco.1995.1131","volume":"121","author":"L. Bachmair","year":"1995","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation. Information and Computation\u00a0121(2), 172\u2013192 (1995)","journal-title":"Information and Computation"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Bofill, M., Godoy, G., Nieuwenhuis, R., Rubio, A.: Paramodulation with non-monotonic orderings. In: 14th IEEE Symposium on Logic in Computer Science (LICS), Trento, Italy, July 2-5, vol.\u00a05, pp. 225\u2013233 (1999)","DOI":"10.1109\/LICS.1999.782618"},{"key":"1_CR28","unstructured":"Bertling, H., Ganzinger, H., Sch\u00e4fers, R.: CEC: A system for conditional equational completion \u2014 User manual, version 1.0 (1988)"},{"key":"1_CR29","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)"},{"key":"1_CR30","unstructured":"Bertling, H., Ganzinger, H., Sch\u00e4fers, R.: A collection of specifications completed by the CEC-system, version 1.0 (1988)"},{"key":"1_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0014420","volume-title":"Recent Trends in Data Type Specification","author":"L. Bachmair","year":"1995","unstructured":"Bachmair, L., Ganzinger, H., Stuber, J.: Combining Algebra and Universal Algebra in First-order Theorem Proving: The Case of Commutative Rings. In: Reggio, G., Astesiano, E., Tarlecki, A. (eds.) Abstract Data Types 1994 and COMPASS 1994. LNCS, vol.\u00a0906, pp. 1\u201329. Springer, Heidelberg (1995)"},{"key":"1_CR32","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/BFb0054259","volume-title":"Automated Deduction - CADE-15","author":"L. Bachmair","year":"1998","unstructured":"Bachmair, L., Ganzinger, H., Voronkov, A.: Elimination of Equality via Transformation with Ordering Constraints. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 175\u2013190. Springer, Heidelberg (1998)"},{"key":"1_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/BFb0013841","volume-title":"Algebraic and Logic Programming","author":"L. Bachmair","year":"1992","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Theorem Proving for Hierarchic First-order Theories. In: Kirchner, H., Levi, G. (eds.) ALP 1992. LNCS, vol.\u00a0632, pp. 420\u2013434. Springer, Heidelberg (1992)"},{"key":"1_CR34","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Set constraints are the monadic class. In: Eighth Annual IEEE Symposium on Logic in Computer Science (LICS), Montreal, Canada, pp. 75\u201383. IEEE Computer Society Press (1993)","DOI":"10.1109\/LICS.1993.287598"},{"key":"1_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/BFb0022557","volume-title":"Computational Logic and Proof Theory","author":"L. Bachmair","year":"1993","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Superposition with Simplification as a Decision Procedure for the Monadic Class with Equality. In: Mundici, D., Gottlob, G., Leitsch, A. (eds.) KGC 1993. LNCS, vol.\u00a0713, pp. 83\u201396. Springer, Heidelberg (1993)"},{"key":"1_CR36","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.\u00a05, 193\u2013212 (1994)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"issue":"1","key":"1_CR37","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1006\/inco.2000.2875","volume":"159","author":"H. Comon","year":"2000","unstructured":"Comon, H., Nieuwenhuis, R.: Induction = I-Axiomatization + First-Order Consistency. Information & Computation\u00a0159(1), 151\u2013186 (2000)","journal-title":"Information & Computation"},{"issue":"1","key":"1_CR38","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1145\/1119439.1119443","volume":"7","author":"A. Degtyarev","year":"2006","unstructured":"Degtyarev, A., Fisher, M., Konev, B.: Monodic temporal resolution. ACM Trans. Comput. Log.\u00a07(1), 108\u2013150 (2006)","journal-title":"ACM Trans. Comput. Log."},{"key":"1_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-24364-6_9","volume-title":"Frontiers of Combining Systems","author":"A. Eggers","year":"2011","unstructured":"Eggers, A., Kruglov, E., Kupferschmid, S., Scheibler, K., Teige, T., Weidenbach, C.: Superposition Modulo Non-linear Arithmetic. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS, vol. 6989, pp. 119\u2013134. Springer, Heidelberg (2011)"},{"key":"1_CR40","doi-asserted-by":"crossref","unstructured":"Ganzinger, H.: Darstellung der Artanpassung in h\u00f6heren Programmiersprachen durch Repr\u00e4sentation von Gruppen. In: Schneider, H.J., Nagl, M. (eds.) Programmiersprachen, 4. Fachtagung der GI, Erlangen, Proceedings, M\u00e4rz 8-10. Informatik-Fachberichte, vol. 1, pp. 194\u2013202. Springer (1976)","DOI":"10.1007\/978-3-642-66319-2_19"},{"key":"1_CR41","doi-asserted-by":"crossref","unstructured":"Ganzinger, H.: An approach to the derivation of compiler description concepts from the mathematical semantics concept. In: B\u00f6hling, K.-H., Spies, P.P. (eds.) GI - 9. Jahrestagung, Bonn, Proceedings, Oktober 1-5. Informatik-Fachberichte, vol.\u00a019, pp. 206\u2013217. Springer (1979)","DOI":"10.1007\/978-3-642-67444-0_19"},{"key":"1_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1007\/3-540-09118-1_15","volume-title":"Theoretical Computer Science","author":"H. Ganzinger","year":"1979","unstructured":"Ganzinger, H.: On Storage Optimization for Automatically Generated Compilers. In: Weihrauch, K. (ed.) GI-TCS 1979. LNCS, vol.\u00a067, pp. 132\u2013141. Springer, Heidelberg (1979)"},{"key":"1_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-10250-7_18","volume-title":"Semantics-Directed Compiler Generation","author":"H. Ganzinger","year":"1980","unstructured":"Ganzinger, H.: Transforming denotational semantics into practical attribute grammars. In: Jones, N.D. (ed.) Semantics-Directed Compiler Generation. LNCS, vol.\u00a094, pp. 1\u201369. Springer, Heidelberg (1980)"},{"key":"1_CR44","doi-asserted-by":"crossref","unstructured":"Ganzinger, H.: Description of parameterized compiler modules. In: Brauer, W. (ed.) GI - 11. Jahrestagung in Verbindung mit Third Conference of the European Co-operation in Informatics (ECI), M\u00fcnchen, Proceedings, Oktober 20.-23. Informatik-Fachberichte, vol.\u00a050, pp. 11\u201319. Springer (1981)","DOI":"10.1007\/978-3-662-01089-1_2"},{"issue":"3","key":"1_CR45","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0167-6423(83)90021-7","volume":"3","author":"H. Ganzinger","year":"1983","unstructured":"Ganzinger, H.: Increasing modularity and language-independency in automatically generated compilers. Sci. Comput. Program.\u00a03(3), 223\u2013278 (1983)","journal-title":"Sci. Comput. Program."},{"key":"1_CR46","unstructured":"Ganzinger, H.: Modular compiler descriptions based on abstract semantic data types. In: Proceedings 2nd Workshop on Abstract Data Types, University of Passau (1983)"},{"key":"1_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/BFb0036912","volume-title":"Automata, Languages and Programming","author":"H. Ganzinger","year":"1983","unstructured":"Ganzinger, H.: Modular Compiler Descriptions Based on Abstract Semantic Data Types (Extended Abstract). In: D\u00edaz, J. (ed.) ICALP 1983. LNCS, vol.\u00a0154, pp. 237\u2013249. Springer, Heidelberg (1983)"},{"issue":"3","key":"1_CR48","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1145\/2166.357212","volume":"5","author":"H. Ganzinger","year":"1983","unstructured":"Ganzinger, H.: Parameterized specifications: Parameter passing and implementation with respect to observability. ACM Transactions on Programming Languages and Systems\u00a05(3), 318\u2013354 (1983)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR49","unstructured":"Ganzinger, H.: Knuth-Bendix completion for parametric specifications with conditional equations. In: Workshop on Specification of Abstract Data Types, ADT (1986)"},{"key":"1_CR50","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":"1_CR51","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":"1_CR52","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., Wirsing, M., Vidal-Naquet, G. (eds.) STACS 1987. LNCS, vol.\u00a0247, pp. 286\u2013298. Springer, Heidelberg (1987)"},{"key":"1_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/3-540-50939-9_136","volume-title":"TAPSOFT \u201989. Proceedings of the International Joint Conference on Theory and Practice of Software Development, Barcelona, Spain, March 13-17, 1989","author":"H. Ganzinger","year":"1989","unstructured":"Ganzinger, H.: Order-sorted Completion: The Many-sorted Way (Extended Abstract). In: D\u00edaz, J., Yu, Y. (eds.) CAAP 1989 and TAPSOFT 1989. LNCS, vol.\u00a0351, pp. 244\u2013258. Springer, Heidelberg (1989)"},{"key":"1_CR54","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":"1_CR55","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":"1_CR56","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/3-540-45620-1_28","volume-title":"Automated Deduction - CADE-18","author":"H. Ganzinger","year":"2002","unstructured":"Ganzinger, H.: Shostak Light. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 332\u2013346. Springer, Heidelberg (2002)"},{"key":"1_CR57","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: 14th IEEE Symposium on Logic in Computer Science (LICS), Trento, Italy, July\u00a02\u20135, pp. 295\u2013305 (1999)","DOI":"10.1109\/LICS.1999.782624"},{"key":"1_CR58","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Giegerich, R., M\u00f6ncke, U., Wilhelm, R.: A truly generative semantics-directed compiler generator. In: SIGPLAN Symposium on Compiler Construction, pp. 172\u2013184 (1982)","DOI":"10.1145\/872726.806993"},{"issue":"4","key":"1_CR59","first-page":"241","volume":"29","author":"H. Ganzinger","year":"1987","unstructured":"Ganzinger, H., Heeg, G., Baumeister, H., R\u00fcger, M.: Smalltalk-80. Informationstechnik \u2014 IT\u00a029(4), 241\u2013251 (1987)","journal-title":"Informationstechnik \u2014 IT"},{"key":"1_CR60","unstructured":"Ganzinger, H., Hustadt, U., Meyer, C., Schmidt, R.A.: A resolution-based decision procedure for extensions of K4. In: Zakharyaschev, M., Segerberg, K., de Rijke, M., Wansing, H. (eds.) Advances in Modal Logic 2, Papers from the Second Workshop on Advances in Modal Logic, Uppsala, Sweden, pp. 225\u2013246. CSLI Publications (1998)"},{"key":"1_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast Decision Procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"key":"1_CR62","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-540-45085-6_15","volume-title":"Automated Deduction \u2013 CADE-19","author":"H. Ganzinger","year":"2003","unstructured":"Ganzinger, H., Hillenbrand, T., Waldmann, U.: Superposition Modulo a Shostak Theory. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 182\u2013196. Springer, Heidelberg (2003)"},{"issue":"1","key":"1_CR63","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1142\/S012905410000003X","volume":"11","author":"H. Ganzinger","year":"2000","unstructured":"Ganzinger, H., Jacquemard, F., Veanes, M.: Rigid reachability, the non-symmetric form of rigid E-unification. Int. J. Found. Comput. Sci.\u00a011(1), 3\u201327 (2000)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"1_CR64","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Proc.18th IEEE Symposium on Logic in Computer Science (LICS 2003), pp. 55\u201364. IEEE Computer Society Press (2003)","DOI":"10.1109\/LICS.2003.1210045"},{"key":"1_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-540-30124-0_9","volume-title":"Computer Science Logic","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Korovin, K.: Integrating equational reasoning into instantiation-based theorem proving. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 71\u201384. Springer, Heidelberg (2004)"},{"key":"1_CR66","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/11916277_34","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"H. Ganzinger","year":"2006","unstructured":"Ganzinger, H., Korovin, K.: Theory Instantiation. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 497\u2013511. Springer, Heidelberg (2006)"},{"key":"1_CR67","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Meyer, C., Veanes, M.: The two-variable guarded fragment with transitive relations. In: 14th IEEE Symposium on Logic in Computer Science (LICS), Trento, Italy, July 2-5, pp. 24\u201334 (1999)","DOI":"10.1109\/LICS.1999.782582"},{"key":"1_CR68","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)"},{"key":"1_CR69","doi-asserted-by":"crossref","unstructured":"Godoy, G., Nieuwenhuis, R.: Paramodulation with built-in abelian groups. In: 15th IEEE Symp. Logic in Computer Science (LICS), Santa Barbara, USA, pp. 413\u2013424. IEEE Computer Society Press (2000)","DOI":"10.1109\/LICS.2000.855788"},{"key":"1_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/3-540-45406-3_4","volume-title":"Constraints in Computational Logics. Theory and Applications","author":"H. Ganzinger","year":"2001","unstructured":"Ganzinger, H., Nieuwenhuis, R.: Constraints and Theorem Proving. In: Comon, H., March\u00e9, C., Treinen, R. (eds.) CCL 1999. LNCS, vol.\u00a02002, pp. 159\u2013201. Springer, Heidelberg (2001)"},{"key":"1_CR71","doi-asserted-by":"crossref","unstructured":"Godoy, G., Nieuwenhuis, R.: Ordering Constraints for Deduction with Built-in Abelian Semigroups, Monoids and Groups. In: 16th IEEE Symposium on Logic in Computer Science (LICS), Boston, USA, June 16\u201320, pp. 38\u201347. IEEE Computer Society Press (2001)","DOI":"10.1109\/LICS.2001.932481"},{"issue":"1","key":"1_CR72","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0747-7171(03)00070-1","volume":"37","author":"G. Godoy","year":"2004","unstructured":"Godoy, G., Nieuwenhuis, R.: Superposition with Completely Built-in Abelian Groups. Journ. Symbolic Computation\u00a037(1), 1\u201333 (2004)","journal-title":"Journ. Symbolic Computation"},{"key":"1_CR73","unstructured":"Ganzinger, H., Nieuwenhuis, R., Nivela, P.: The Saturate System (1999), Software and documentation, http:\/\/www.mpi-inf.mpg.de\/SATURATE\/Saturate.html"},{"key":"1_CR74","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Nieuwenhuis, R., Nivela, P.: Context trees. In: EuroGP 2001. LNCS (LNAI), vol.\u00a02038, pp. 242\u2013256, Siena, Italy (2001)","DOI":"10.1007\/3-540-45744-5_18"},{"issue":"2","key":"1_CR75","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. Journal of Automated Reasoning\u00a032(2), 103\u2013120 (2004)","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR76","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"1_CR77","unstructured":"Ganzinger, H., Ripken, K., Wilhelm, R.: Automatic generation of optimizing multipass compilers. In: IFIP Congress, pp. 535\u2013540 (1977)"},{"key":"1_CR78","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/3-540-56393-8_17","volume-title":"Conditional Term Rewriting Systems","author":"H. Ganzinger","year":"1993","unstructured":"Ganzinger, H., Stuber, J.: Inductive Theorem Proving by Consistency for First-order Clauses. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol.\u00a0656, pp. 226\u2013241. Springer, Heidelberg (1993)"},{"issue":"1-2","key":"1_CR79","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. Inf. Comput.\u00a0199(1-2), 3\u201323 (2005)","journal-title":"Inf. Comput."},{"key":"1_CR80","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Sofronie-Stokkermans, V.: Chaining techniques for automated theorem proving in many-valued logics. In: 30th IEEE International Symposium on Multiple-Valued Logic (ISMV)L, pp. 337\u2013344 (2000)","DOI":"10.1109\/ISMVL.2000.848641"},{"issue":"10","key":"1_CR81","doi-asserted-by":"publisher","first-page":"1453","DOI":"10.1016\/j.ic.2005.10.002","volume":"204","author":"H. Ganzinger","year":"2006","unstructured":"Ganzinger, H., Sofronie-Stokkermans, V., Waldmann, U.: Modular proof systems for partial functions with Evans equality. Inf. Comput.\u00a0204(10), 1453\u20131492 (2006)","journal-title":"Inf. Comput."},{"key":"1_CR82","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"654","DOI":"10.1007\/3-540-07410-4_666","volume-title":"GI Jahrestagung","author":"H. Ganzinger","year":"1975","unstructured":"Ganzinger, H., Wilhelm, R.: Verschr\u00e4nkung von Compiler-Moduln. In: M\u00fchlbacher, J.R. (ed.) GI 1975. LNCS, vol.\u00a034, pp. 654\u2013665. Springer, Heidelberg (1975)"},{"key":"1_CR83","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/3-540-56393-8_34","volume-title":"Conditional Term Rewriting Systems","author":"H. Ganzinger","year":"1993","unstructured":"Ganzinger, H., Waldmann, U.: Termination Proofs of Well-moded Logic Programs via Conditional Rewrite Systems. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol.\u00a0656, pp. 430\u2013437. Springer, Heidelberg (1993)"},{"key":"1_CR84","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/3-540-61511-3_102","volume-title":"Automated Deduction - Cade-13","author":"H. Ganzinger","year":"1996","unstructured":"Ganzinger, H., Waldmann, U.: Theorem Proving in Cancellative Abelian Monoids. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol.\u00a01104, pp. 388\u2013402. Springer, Heidelberg (1996)"},{"key":"#cr-split#-1_CR85.1","unstructured":"Herbrand, J.: Recherches sur la th\u00e9orie de la d\u00e9monstration. Traveaux de la Societ\u00e9 des Sciences de Varsoria\u00a033 (1930)"},{"key":"#cr-split#-1_CR85.2","unstructured":"Translation appeared in van Heijenoort, J.: From Frege to G\u00f6del: A Source Book in Mathematical Logic, pp. 525-581. Harvard University Press (1967)"},{"key":"1_CR86","unstructured":"Hillenbrand, T.: Superposition and Decision Procedures \u2013 Back and Forth. PhD thesis, Universit\u00e4t des Saarlandes (2008)"},{"key":"1_CR87","series-title":"Lecture Notes in Computer Science","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, vol.\u00a06173, pp. 188\u2013195. Springer, Heidelberg (2010)"},{"issue":"5","key":"1_CR88","doi-asserted-by":"publisher","first-page":"579","DOI":"10.1016\/j.ic.2007.11.006","volume":"206","author":"U. Hustadt","year":"2008","unstructured":"Hustadt, U., Motik, B., Sattler, U.: Deciding expressive description logics in the framework of resolution. Inf. Comput.\u00a0206(5), 579\u2013601 (2008)","journal-title":"Inf. Comput."},{"key":"1_CR89","unstructured":"Hillenbrand, T., Weidenbach, C.: Superposition for finite domains. Research Report MPI-I-2007-RG1-002, Max-Planck Institute for Informatics, Saarbruecken, Germany (April 2007)"},{"issue":"4","key":"1_CR90","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1805950.1805957","volume":"11","author":"M. Horbach","year":"2010","unstructured":"Horbach, M., Weidenbach, C.: Superposition for fixed domains. ACM Transactions on Computational Logic\u00a011(4), 1\u201335 (2010)","journal-title":"ACM Transactions on Computational Logic"},{"key":"1_CR91","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":"1_CR92","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1007\/11814771_45","volume-title":"Automated Reasoning","author":"F. Jacquemard","year":"2006","unstructured":"Jacquemard, F., Rusinowitch, M., Vigneron, L.: Tree Automata with Equality Constraints Modulo Equational Theories. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 557\u2013571. Springer, Heidelberg (2006)"},{"key":"1_CR93","doi-asserted-by":"crossref","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, I. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"issue":"3","key":"1_CR94","first-page":"9","volume":"4","author":"C. Kirchner","year":"1990","unstructured":"Kirchner, C., Kirchner, H., Rusinowitch, M.: Deduction with symbolic constraints. Revue Fran\u00e7aise d\u2019Intelligence Artificielle\u00a04(3), 9\u201352 (1990)","journal-title":"Revue Fran\u00e7aise d\u2019Intelligence Artificielle"},{"issue":"2-3","key":"1_CR95","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10817-007-9090-1","volume":"40","author":"Y. Kazakov","year":"2008","unstructured":"Kazakov, Y., Motik, B.: A resolution-based decision procedure for shoiq. Journal of Automated Reasoning\u00a040(2-3), 89\u2013116 (2008)","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"1_CR96","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/S0747-7171(88)80019-1","volume":"6","author":"D. Kapur","year":"1988","unstructured":"Kapur, D., Musser, D.R., Narendran, P.: Only prime superpositions need be considered in the Knuth-Bendix completion procedure. Journal of Symbolic Computation\u00a06(1), 19\u201336 (1988)","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR97","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-74915-8_19","volume-title":"Computer Science Logic","author":"K. Korovin","year":"2007","unstructured":"Korovin, K., Voronkov, A.: Integrating Linear Arithmetic into Superposition Calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 223\u2013237. Springer, Heidelberg (2007)"},{"key":"1_CR98","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-540-73595-3_21","volume-title":"Automated Deduction \u2013 CADE-21","author":"T. Lev-Ami","year":"2007","unstructured":"Lev-Ami, T., Weidenbach, C., Reps, T.W., Sagiv, M.: Labelled Clauses. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 311\u2013327. Springer, Heidelberg (2007)"},{"issue":"2","key":"1_CR99","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/0304-3975(94)00274-6","volume":"142","author":"C. Lynch","year":"1995","unstructured":"Lynch, C., Snyder, W.: Redundancy criteria for constrained completion. Theoretical Compututer Science\u00a0142(2), 141\u2013177 (1995)","journal-title":"Theoretical Compututer Science"},{"issue":"1-2","key":"1_CR100","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1006\/inco.2000.2877","volume":"159","author":"J. Levy","year":"2000","unstructured":"Levy, J., Veanes, M.: On the undecidability of second-order unification. Inf. Comput.\u00a0159(1-2), 125\u2013150 (2000)","journal-title":"Inf. Comput."},{"issue":"2","key":"1_CR101","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1145\/151261.151265","volume":"40","author":"D. McAllester","year":"1993","unstructured":"McAllester, D.: Automatic recognition of tractability in inferences relations. Journal of the ACM\u00a040(2), 284\u2013303 (1993)","journal-title":"Journal of the ACM"},{"issue":"3","key":"1_CR102","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W. McCune","year":"1997","unstructured":"McCune, W.: Solution of the Robbins problem. Journal of Automated Reasoning\u00a019(3), 263\u2013276 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR103","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"1_CR104","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R.: Basic paramodulation and decidable theories. In: Eleventh Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, pp. 473\u2013482. IEEE Computer Society Press (1996)","DOI":"10.1109\/LICS.1996.561464"},{"key":"1_CR105","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1007\/3-540-61511-3_125","volume-title":"Automated Deduction - Cade-13","author":"T. Nipkow","year":"1996","unstructured":"Nipkow, T.: More Church-Rosser Proofs (in Isabelle\/HOL). In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 733\u2013747. Springer, Heidelberg (1996)"},{"key":"1_CR106","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.: Practical Results on the Saturation of Full First-order Clauses: Experiments with the Saturate System (System Description). In: Kirchner, C. (ed.) RTA 1993. LNCS, vol.\u00a0690, pp. 436\u2013440. Springer, Heidelberg (1993)"},{"key":"1_CR107","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/3-540-55253-7_22","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, pp. 371\u2013390. Springer, Heidelberg (1992)"},{"key":"1_CR108","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1007\/3-540-55602-8_186","volume-title":"Automated Deduction - CADE-11","author":"R. Nieuwenhuis","year":"1992","unstructured":"Nieuwenhuis, R., Rubio, A.: Theorem Proving with Ordering Constrained Clauses. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 477\u2013491. Springer, Heidelberg (1992)"},{"key":"1_CR109","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/3-540-58156-1_40","volume-title":"Automated Deduction - CADE-12","author":"R. Nieuwenhuis","year":"1994","unstructured":"Nieuwenhuis, R., Rubio, A.: AC-Superposition with Constraints: No AC-unifiers Needed. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814, pp. 545\u2013559. Springer, Heidelberg (1994)"},{"issue":"4","key":"1_CR110","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1006\/jsco.1995.1020","volume":"19","author":"R. Nieuwenhuis","year":"1995","unstructured":"Nieuwenhuis, R., Rubio, A.: Theorem Proving with Ordering and Equality Constrained Clauses. Journal of Symbolic Computation\u00a019(4), 321\u2013351 (1995)","journal-title":"Journal of Symbolic Computation"},{"issue":"1","key":"1_CR111","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 J. on Computing\u00a012(1), 82\u2013100 (1983)","journal-title":"SIAM J. on Computing"},{"issue":"1","key":"1_CR112","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM\u00a012(1), 23\u201341 (1965)","journal-title":"Journal of the ACM"},{"key":"1_CR113","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Communications\u00a015(91-110) (2002)"},{"key":"1_CR114","first-page":"135","volume":"4","author":"G.A. Robinson","year":"1969","unstructured":"Robinson, G.A., Wos, L.T.: Paramodulation and theorem-proving in first order theories with equality. Machine Intelligence\u00a04, 135\u2013150 (1969)","journal-title":"Machine Intelligence"},{"key":"1_CR115","unstructured":"Schulz, S., Bonacina, M.P.: On handling distinct objects in the superposition calculus. In: Notes 5th IWIL Workshop on the Implementation of Logics, pp. 11\u201366 (2005)"},{"issue":"2\/3","key":"1_CR116","first-page":"111","volume":"15","author":"E. Stephan Schulz","year":"2002","unstructured":"Stephan Schulz, E.: A Brainiac Theorem Prover. Journal of AI Communications\u00a015(2\/3), 111\u2013126 (2002)","journal-title":"Journal of AI Communications"},{"key":"1_CR117","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/10721959_34","volume-title":"Automated Deduction - CADE-17","author":"R.A. Schmidt","year":"2000","unstructured":"Schmidt, R.A., Hustadt, U.: A Resolution Decision Procedure for Fluted Logic. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 433\u2013448. Springer, Heidelberg (2000)"},{"issue":"4","key":"1_CR118","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1276920.1276921","volume":"8","author":"R.A. Schmidt","year":"2007","unstructured":"Schmidt, R.A., Hustadt, U.: The axiomatic translation principle for modal logic. ACM Trans. Comput. Log.\u00a08(4), 1\u201351 (2007)","journal-title":"ACM Trans. Comput. Log."},{"key":"1_CR119","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-642-28729-9_11","volume-title":"Foundations of Software Science and Computational Structures","author":"H. Seidl","year":"2012","unstructured":"Seidl, H., Reu\u00df, A.: Extending ${\\cal H}_1$ -Clauses with Path Disequalities. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol.\u00a07213, pp. 165\u2013179. Springer, Heidelberg (2012)"},{"issue":"1-2","key":"1_CR120","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0304-3975(98)00082-6","volume":"208","author":"J. Stuber","year":"1998","unstructured":"Stuber, J.: Superposition theorem proving for abelian groups represented as integer modules. Theoretical Computer Science\u00a0208(1-2), 149\u2013177 (1998)","journal-title":"Theoretical Computer Science"},{"key":"1_CR121","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-94-017-0437-3_2","volume-title":"Automated Deduction - A Basis for Applications","author":"J. Stuber","year":"1998","unstructured":"Stuber, J.: Superposition theorem proving for commutative rings. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction - A Basis for Applications, vol.\u00a0III. Applications, ch.2, pp. 31\u201355. Kluwer, Dordrecht (1998)"},{"key":"1_CR122","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/978-3-642-31365-3_42","volume-title":"Automated Reasoning","author":"M. Suda","year":"2012","unstructured":"Suda, M., Weidenbach, C.: A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 537\u2013543. Springer, Heidelberg (2012)"},{"key":"1_CR123","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-642-14203-1_38","volume-title":"Automated Reasoning","author":"M. Suda","year":"2010","unstructured":"Suda, M., Weidenbach, C., Wischnewski, P.: On the Saturation of YAGO. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol.\u00a06173, pp. 441\u2013456. Springer, Heidelberg (2010)"},{"key":"1_CR124","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/3-540-48242-3_9","volume-title":"Logic Programming and Automated Reasoning","author":"U. Waldmann","year":"1999","unstructured":"Waldmann, U.: Cancellative Superposition Decides the Theory of Divisible Torsion-free Abelian Groups. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS (LNAI), vol.\u00a01705, pp. 131\u2013147. Springer, Heidelberg (1999)"},{"key":"1_CR125","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1007\/3-540-45744-5_17","volume-title":"Proceedings of the International Joint Conference on Automated Reasoning (IJCAR 2001)","author":"U. Waldmann","year":"2001","unstructured":"Waldmann, U.: Superposition and Chaining for Totally Ordered Divisible Abelian Groups. In: Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) EuroGP 2001. LNCS, vol.\u00a02038, pp. 226\u2013241. Springer, Heidelberg (2001), www.mpi-inf.mpg.de\/~uwe\/paper\/IJCAR01-bibl.html"},{"issue":"2","key":"1_CR126","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1023\/A:1005812220011","volume":"18","author":"C. Weidenbach","year":"1997","unstructured":"Weidenbach, C.: SPASS\u2014version 0.49. Journal of Automated Reasoning\u00a018(2), 247\u2013252 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR127","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":"1_CR128","unstructured":"Wilhelm, R., Ripken, K., Ciesinger, J., Ganzinger, H., Lahner, W., Nollmann, R.: Design evaluation of the compiler generating system MUGI. In: Yeh, R.T., Ramamoorthy, C.V. (eds.) Proceedings of the 2nd International Conference on Software Engineering, San Francisco, California, USA, 1976, October 13-15, pp. 571\u2013576. IEEE Computer Society (1976)"},{"issue":"4","key":"1_CR129","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. Journal of the ACM\u00a014(4), 698\u2013709 (1967)","journal-title":"Journal of the ACM"},{"key":"1_CR130","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-540-73595-3_38","volume-title":"Automated Deduction \u2013 CADE-21","author":"C. Weidenbach","year":"2007","unstructured":"Weidenbach, C., Schmidt, R.A., Hillenbrand, T., Rusev, R., Topic, D.: System Description: Spass Version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 514\u2013520. Springer, Heidelberg (2007)"},{"issue":"2-3","key":"1_CR131","doi-asserted-by":"crossref","first-page":"97","DOI":"10.3233\/AIC-2010-0459","volume":"23","author":"C. Weidenbach","year":"2010","unstructured":"Weidenbach, C., Wischnewski, P.: Subterm contextual rewriting. AI Communications\u00a023(2-3), 97\u2013109 (2010)","journal-title":"AI Communications"},{"key":"1_CR132","unstructured":"Zhang, H.: Reduction, superposition and induction: Automated reasoning in an equational logic. Research Report 88\u201306, University of Iowa (November 1988)"},{"key":"1_CR133","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.\u2018., Overbeek, R. (eds.) CADE 1988. LNCS, vol.\u00a0310, pp. 1\u201320. Springer, Heidelberg (1988)"},{"key":"1_CR134","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/3-540-51081-8_129","volume-title":"Rewriting Techniques and Applications","author":"H. Zhang","year":"1989","unstructured":"Zhang, H., Kapur, D.: Consider only General Superpositions in Completion Procedures. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol.\u00a0355, pp. 513\u2013527. Springer, Heidelberg (1989)"},{"issue":"3","key":"1_CR135","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/BF02090774","volume":"23","author":"H. Zhang","year":"1990","unstructured":"Zhang, H., Kapur, D.: Unnecessary inferences in associative-commutative completion procedures. Mathematical Systems Theory\u00a023(3), 175\u2013206 (1990)","journal-title":"Mathematical Systems Theory"},{"key":"1_CR136","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/3-540-15976-2_2","volume-title":"Rewriting Techniques and Applications","author":"H. Zhang","year":"1985","unstructured":"Zhang, H., Remy, J.-L.: Contextual Rewriting. In: Jouannaud, J.-P. (ed.) RTA 1985. LNCS, vol.\u00a0202, pp. 46\u201362. Springer, Heidelberg (1985)"}],"container-title":["Lecture Notes in Computer Science","Programming Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-37651-1_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T03:17:47Z","timestamp":1745983067000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-37651-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642376504","9783642376511"],"references-count":137,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-37651-1_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}