{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:21Z","timestamp":1749125181145},"publisher-location":"Berlin, Heidelberg","reference-count":61,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540616306"},{"type":"electronic","value":"9783540706434"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61630-6_4","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:09:24Z","timestamp":1330294164000},"page":"50-69","source":"Crossref","is-referenced-by-count":7,"title":["What you always wanted to know about rigid E-unification"],"prefix":"10.1007","author":[{"given":"Anatoli","family":"Degtyarev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"issue":"2","key":"4_CR1","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P.B. Andrews","year":"1981","unstructured":"P.B. Andrews. Theorem proving via general matings. Journal of the Association for Computing Machinery, 28(2):193\u2013214, 1981.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"4_CR2","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/BF00881838","volume":"10","author":"A. Avron","year":"1993","unstructured":"A. Avron. Gentzen-type systems, resolution and tableaux. Journal of Automated Reasoning, 10:256\u2013281, 1993.","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR3","first-page":"462","volume-title":"volume 607 of Lecture Notes in Artificial Intelligence","author":"L. Bachmair","year":"1992","unstructured":"L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic paramodulation and superposition. In D. Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 462\u2013476, Saratoga Springs, NY, USA, June 1992. Springer Verlag."},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1006\/inco.1995.1131","volume":"121","author":"L. Bachmair","year":"1995","unstructured":"L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basis paramodulation. Information and Computation, 121:172\u2013192, 1995.","journal-title":"Information and Computation"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Peter Baumgartner. An ordered theory resolution calculus. In A. Voronkov, editor, Logic Programming and Automated Reasoning (LPAR'92), volume 624 of Lecture Notes in Computer Science, pages 119\u2013130, 1992.","DOI":"10.1007\/BFb0013054"},{"key":"4_CR6","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1006\/jsco.1993.1058","volume":"16","author":"P. Baumgartner","year":"1993","unstructured":"P. Baumgartner and U. Furbach. Consolution as a framework for comparing calculi. Journal of Symbolic Computations, 16:445\u2013477, 1993.","journal-title":"Journal of Symbolic Computations"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"P. Baumgartner and U. Furbach. PROTEIN: A PROver with a Theory Extension INterface. In A. Bundy, editor, Automated Deduction \u2014 CADE-12. 12th International Conference on Automated Deduction., volume 814 of Lecture Notes in Artificial Intelligence, pages 769\u2013773, Nancy, France, June\/July 1994.","DOI":"10.1007\/3-540-58156-1_57"},{"key":"4_CR8","first-page":"319","volume-title":"volume 861 of Lecture Notes in Artificial Intelligence","author":"G. Becher","year":"1994","unstructured":"G. Becher and U. Petermann. Rigid unification by completion and rigid paramodulation. In B. Nebel and L. Dreschler-Fischer, editors, KI-94: Advances in Artificial Intelligence. 18th German Annual Conference on Artificial Intelligence, volume 861 of Lecture Notes in Artificial Intelligence, pages 319\u2013330, Saarbr\u00fccken, Germany, September 1994. Springer Verlag."},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"B. Beckert. A completion-based method for mixed universal and rigid E-unification. In A. Bundy, editor, Automated Deduction \u2014 CADE-12. 12th International Conference on Automated Deduction., volume 814 of Lecture Notes in Artificial Intelligence, pages 678\u2013692, Nancy, France, June\/July 1994.","DOI":"10.1007\/3-540-58156-1_49"},{"key":"4_CR10","unstructured":"B. Beckert. Are minimal solutions to simultaneous rigid E-unification sufficient for adding equality to semantic tableaux? Privately circulated manuscript, University of Karlsruhe, 1995."},{"key":"4_CR11","first-page":"678","volume-title":"volume 607 of Lecture Notes in Artificial Intelligence","author":"B. Beckert","year":"1992","unstructured":"B. Beckert and R. H\u00e4hnle. An improved method for adding equality to free variable semantic tableaux. In D. Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 678\u2013692, Saratoga Springs, NY, USA, June 1992. Springer Verlag."},{"issue":"4","key":"4_CR12","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1145\/322276.322277","volume":"28","author":"W. Bibel","year":"1981","unstructured":"W. Bibel. On matrices with connections. Journal of the Association for Computing Machinery, 28(4):633\u2013645, 1981.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"W. Bibel. Issues in theorem proving based on the connection method. In P. Baumgartner, R. H\u00e4hnle, and J. Posegga, editors, Theorem Proving with Analytic Tableaux and Related Methods, number 918 in Lecture Notes in Artificial Intelligence, pages 1\u201316, Schlo\u00df Rheinfels, St. Goar, Germany, May 1995.","DOI":"10.1007\/3-540-59338-1_24"},{"key":"4_CR14","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"D. Brand. Proving theorems with the modification method. SIAM Journal of Computing, 4:412\u2013430, 1975.","journal-title":"SIAM Journal of Computing"},{"key":"4_CR15","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/S0020-0255(72)80012-4","volume":"4","author":"C.L. Chang","year":"1972","unstructured":"C.L. Chang. Theorem proving with variable-constrained resolution. Information Sciences, 4:217\u2013231, 1972.","journal-title":"Information Sciences"},{"key":"4_CR16","unstructured":"A. Degtyarev. The strategy of monotone paramodulation (in Russian). In Fifth Soviet All-Union Conference on Mathematical Logic, page 39, Novosibirsk, 1979."},{"key":"4_CR17","first-page":"14","volume-title":"Automation of Research in Mathematics","author":"A. Degtyarev","year":"1982","unstructured":"A. Degtyarev. On the forms of inference in calculi with equality and paramodulation (in Russian). In Yu.V. Kapitonova, editor, Automation of Research in Mathematics, pages 14\u201326. Institute of Cybernetics, Kiev, 1982."},{"key":"4_CR18","unstructured":"A. Degtyarev, Yu. Matiyasevich, and A. Voronkov. Simultaneous rigid E-unification and related algorithmic problems. To appear in LICS'96, 9 pages, 1996."},{"key":"4_CR19","unstructured":"A. Degtyarev and A. Voronkov. Equality elimination for semantic tableaux. UPMAIL Technical Report 90, Uppsala University, Computing Science Department, December 1994. To appear in DISCO'96."},{"key":"4_CR20","unstructured":"A. Degtyarev and A. Voronkov. General connections via equality elimination. UPMAIL Technical Report 93, Uppsala University, Computing Science Department, January 1995."},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"A. Degtyarev and A. Voronkov. Simultaneous rigid E-unification is undecidable. UPMAIL Technical Report 105, Uppsala University, Computing Science Department, May 1995. To appear in Theoretical Computer Science, v.166, 1996.","DOI":"10.1016\/0304-3975(96)00092-8"},{"key":"4_CR22","unstructured":"A. Degtyarev and A. Voronkov. Reduction of second-order unification to simultaneous rigid E-unification. UPMAIL Technical Report 109, Uppsala University, Computing Science Department, June 1995."},{"key":"4_CR23","first-page":"109","volume-title":"General connections via equality elimination","author":"A. Degtyarev","year":"1995","unstructured":"A. Degtyarev and A. Voronkov. General connections via equality elimination. In M. De Glas and Z. Pawlak, editors, Second World Conference on the Fundamentals of Artificial Intelligence (WOCFAI-95), pages 109\u2013120, Paris, July 1995. Angkor."},{"key":"4_CR24","unstructured":"A. Degtyarev and A. Voronkov. Equality elimination for the inverse method and extension procedures. In C.S. Mellish, editor, Proc. International Joint Conference on Artificial Intelligence (IJCAI), volume 1, pages 342\u2013347, Montr\u00e9al, August 1995."},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"A. Degtyarev and A. Voronkov. Handling equality in logic programs via basic folding. In R. Dyckhoff, H. Herre, and P. Schroeder-Heister, editors, Extensions of Logic Programming (5th International Workshop, ELP'96), volume 1050 of Lecture Notes in Computer Science, pages 119\u2013136, Leipzig, Germany, March 1996.","DOI":"10.1007\/3-540-60983-0_8"},{"key":"4_CR26","unstructured":"A. Degtyarev and A. Voronkov. Decidability problems for the prenex fragment of intuitionistic logic. To appear in LICS'96, 10 pages, 1996."},{"key":"4_CR27","unstructured":"A. Degtyarev and A. Voronkov. What you always wanted to know about rigid E-unification. UPMAIL Technical Report, Uppsala University, Computing Science Department, to appear."},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"E. De Kogel. Rigid E-unification simplified. In P. Baumgartner, R. H\u00e4hnle, and J. Posegga, editors, Theorem Proving with Analytic Tableaux and Related Methods, number 918 in Lecture Notes in Artificial Intelligence, pages 17\u201330, Schlo\u00df Rheinfels, St. Goar, Germany, May 1995.","DOI":"10.1007\/3-540-59338-1_25"},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"E. Eder. A comparison of the resolution calculus and the connection method, and a new calculus generalizing both methods. In E. B\u00f6rger, G. J\u00e4ger, H. Kleine B\u00fcning, and M.M. Richter, editors, CSL'88 (Proc. 2nd Workshop on Computer Science Logic), volume 385 of Lecture Notes in Computer Science, pages 80\u201398. Springer Verlag, 1988.","DOI":"10.1007\/BFb0026296"},{"key":"4_CR30","unstructured":"E. Eder. Consolution and its relation with resolution. In Proc. International Joint Conference on Artificial Intelligence (IJCAI), pages 132\u2013136, 1991."},{"key":"4_CR31","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-0357-2","volume-title":"First Order Logic and Automated Theorem Proving","author":"M. Fitting","year":"1990","unstructured":"M. Fitting. First Order Logic and Automated Theorem Proving. Springer Verlag, New York, 1990."},{"issue":"1\/2","key":"4_CR32","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/0890-5401(90)90061-L","volume":"87","author":"J. Gallier","year":"1990","unstructured":"J. Gallier, P. Narendran, D. Plaisted, and W. Snyder. Rigid E-unification: NP-completeness and applications to equational matings. Information and Computation, 87(1\/2):129\u2013195, 1990.","journal-title":"Information and Computation"},{"issue":"2","key":"4_CR33","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1145\/128749.128754","volume":"39","author":"J. Gallier","year":"1992","unstructured":"J. Gallier, P. Narendran, S. Raatz, and W. Snyder. Theorem proving using equational matings and rigid E-unification. Journal of the Association for Computing Machinery, 39(2):377\u2013429, 1992.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"J.H. Gallier, P. Narendran, D. Plaisted, and W. Snyder. Rigid E-unification is NP-complete. In Proc. IEEE Conference on Logic in Computer Science (LICS), pages 338\u2013346. IEEE Computer Society Press, July 1988.","DOI":"10.1109\/LICS.1988.5121"},{"key":"4_CR35","unstructured":"J.H. Gallier, S. Raatz, and W. Snyder. Theorem proving using rigid E-unification: Equational matings. In Proc. IEEE Conference on Logic in Computer Science (LICS), pages 338\u2013346. IEEE Computer Society Press, 1987."},{"key":"4_CR36","doi-asserted-by":"crossref","unstructured":"J.H. Gallier, S. Raatz, and W. Snyder. Rigid E-unification and its applications to equational matings. In H. A\u00eft Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, volume 1, pages 151\u2013216. Academic Press, 1989.","DOI":"10.1016\/B978-0-12-046370-1.50011-5"},{"key":"4_CR37","unstructured":"J. Goubault. A rule-based algorithm for rigid E-unification. In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors, Computational Logic and Proof Theory. Proceedings of the Third Kurt G\u00f6del Colloquium, KGC'93, volume 713 of Lecture Notes in Computer Science, pages 202\u2013210, Brno, August 1993."},{"key":"4_CR38","unstructured":"J. Goubault. Rigid E-unifiability is DEXPTIME-complete. In Proc. IEEE Conference on Logic in Computer Science (LICS). IEEE Computer Society Press, 1994."},{"key":"4_CR39","unstructured":"R. H\u00e4hnle, B. Beckert, and S. Gerberding. The many-valued tableau-based theorem prover 3 T AP. Technical Report 30\/94, Universit\u00e4t Karlsruhe, Fakult\u00e4t f\u00fcr Informatik, November 1994."},{"key":"4_CR40","doi-asserted-by":"crossref","unstructured":"S. Kanger. A simplified proof method for elementary logic. In J. Siekmann and G. Wrightson, editors, Automation of Reasoning. Classical Papers on Computational Logic, volume 1, pages 364\u2013371. Springer Verlag, 1983. Originally appeared in 1963.","DOI":"10.1007\/978-3-642-81952-0_23"},{"key":"4_CR41","first-page":"210","volume":"95","author":"J. Kruskal","year":"1960","unstructured":"J. Kruskal. Well quasi ordering, the tree problem and Vazsonyi's conjecture. Transactions of the American Mathematical Society, 95:210\u2013225, 1960.","journal-title":"Transactions of the American Mathematical Society"},{"key":"4_CR42","unstructured":"R.C.T. Lee and C.L. Chang. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973."},{"key":"4_CR43","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D.W. Loveland","year":"1968","unstructured":"D.W. Loveland. Mechanical theorem proving by model elimination. Journal of the Association for Computing Machinery, 15:236\u2013251, 1968.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"4_CR44","unstructured":"D.W. Loveland. Automated Theorem Proving: a Logical Basis. North Holland, 1978."},{"key":"4_CR45","first-page":"1420","volume":"5","author":"S. Maslov","year":"1964","unstructured":"S.Yu. Maslov. The inverse method of establishing deducibility in the classical predicate calculus. Soviet Mathematical Doklady, 5:1420\u20131424, 1964.","journal-title":"Soviet Mathematical Doklady"},{"key":"4_CR46","series-title":"English Translation in: Seminars in Mathematics: Steklov Math. Inst. 4","first-page":"36","volume-title":"Zapiski Nauchnyh Seminarov LOMI, 4","author":"S. Maslov","year":"1969","unstructured":"S.Yu. Maslov. An invertible sequential variant of constructive predicate calculus (in Russian). Zapiski Nauchnyh Seminarov LOMI, 4, 1967. English Translation in: Seminars in Mathematics: Steklov Math. Inst. 4, Consultants Bureau, NY-London, 1969, p. 36\u201342."},{"key":"4_CR47","first-page":"768","volume":"148","author":"V.A. Matulis","year":"1963","unstructured":"V.A. Matulis. On variants of classical predicate calculus with the unique deduction tree (in Russian). Soviet Mathematical Doklady, 148:768\u2013770, 1963.","journal-title":"Soviet Mathematical Doklady"},{"key":"4_CR48","doi-asserted-by":"crossref","unstructured":"G. Mints. Gentzen-type systems and resolution rules. part I. propositional logic. In P. Martin-L\u00f6f and G. Mints, editors, COLOG-88, volume 417 of Lecture Notes in Computer Science, pages 198\u2013231. Springer Verlag, 1990.","DOI":"10.1007\/3-540-52335-9_55"},{"key":"4_CR49","volume-title":"Technical Report AR-95-11","author":"M. Moser","year":"1995","unstructured":"M. Moser, C. Lynch, and J. Steinbach. Model elimination with basic ordered paramodulation. Technical Report AR-95-11, Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen, 1995."},{"key":"4_CR50","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis and A. Rubio. Basic superposition is complete. In ESOP'92, volume 582 of Lecture Notes in Computer Science, pages 371\u2013389. Springer Verlag, 1992.","DOI":"10.1007\/3-540-55253-7_22"},{"key":"4_CR51","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/0020-0190(93)90226-Y","volume":"47","author":"R. Nieuwenhuis","year":"1993","unstructured":"R. Nieuwenhuis. Simple LPO constraint solving methods. Information Processing Letters, 47:65\u201369, 1993.","journal-title":"Information Processing Letters"},{"key":"4_CR52","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1006\/jsco.1995.1020","volume":"19","author":"R. Nieuwenhuis","year":"1995","unstructured":"R. Nieuwenhuis and A. Rubio. Theorem proving with ordering and equality constrained clauses. Journal of Symbolic Computations, 19:321\u2013351, 1995.","journal-title":"Journal of Symbolic Computations"},{"key":"4_CR53","volume-title":"The Theory of Logical Inference","author":"S.A. Norgela","year":"1974","unstructured":"S.A. Norgela. On the size of derivations under minus-normalization (in Russian). In V.A. Smirnov, editor, The Theory of Logical Inference. Institute of Philosophy, Moscow, 1974."},{"key":"4_CR54","doi-asserted-by":"crossref","unstructured":"U. Petermann. A complete connection calculus with rigid E-unification. In JELIA '94, volume 838 of Lecture Notes in Computer Science, pages 152\u2013166, 1994.","DOI":"10.1007\/BFb0021970"},{"key":"4_CR55","unstructured":"D.A. Plaisted. Special cases and substitutes for rigid E-unification. Technical Report MPI-I-95-2-010, Max-Planck-Institut f\u00fcr Informatik, November 1995."},{"key":"4_CR56","doi-asserted-by":"crossref","unstructured":"D. Prawitz. An improved proof procedure. In J. Siekmann and G. Wrightson, editors, Automation of Reasoning. Classical Papers on Computational Logic, volume 1, pages 162\u2013201. Springer Verlag, 1983. Originally appeared in 1960.","DOI":"10.1007\/978-3-642-81952-0_12"},{"key":"4_CR57","first-page":"135","volume-title":"Machine Intelligence, volume 4","author":"G. Robinson","year":"1969","unstructured":"G. Robinson and L.T. Wos. Paramodulation and theorem-proving in first order theories with equality. In Meltzer and Michie, editors, Machine Intelligence, volume 4, pages 135\u2013150. Edinburgh University Press, Edinburgh, 1969."},{"issue":"3","key":"4_CR58","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/BF00881952","volume":"13","author":"J. Schumann","year":"1994","unstructured":"J. Schumann. Tableau-based theorem provers: Systems and implementations. Journal of Automated Reasoning, 13(3):409\u2013421, 1994.","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR59","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1145\/359545.359570","volume":"21","author":"R. Shostak","year":"1978","unstructured":"R. Shostak. An algorithm for reasoning about equality. Communications of the ACM, 21:583\u2013585, July 1978.","journal-title":"Communications of the ACM"},{"key":"4_CR60","doi-asserted-by":"crossref","unstructured":"R.M. Smullyan. First-Order Logic. Springer Verlag, 1968.","DOI":"10.1007\/978-3-642-86718-7"},{"key":"4_CR61","doi-asserted-by":"crossref","unstructured":"A. Voronkov. On proof search in intuitionistic logic with equality, or back to simultaneous rigid E-unification. To appear in CADE'96, 15 pages, 1996.","DOI":"10.1007\/3-540-61511-3_67"}],"container-title":["Lecture Notes in Computer Science","Logics in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61630-6_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:08:57Z","timestamp":1605647337000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61630-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540616306","9783540706434"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/3-540-61630-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}