{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,6]],"date-time":"2025-06-06T04:06:46Z","timestamp":1749182806746,"version":"3.41.0"},"reference-count":63,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[1998,4,1]],"date-time":"1998-04-01T00:00:00Z","timestamp":891388800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,4,1]],"date-time":"1998-04-01T00:00:00Z","timestamp":891388800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[1998,4]]},"DOI":"10.1023\/a:1005996623714","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T00:10:48Z","timestamp":1040515848000},"page":"47-80","source":"Crossref","is-referenced-by-count":21,"title":["What You Always Wanted to Know about Rigid E-Unification"],"prefix":"10.1007","volume":"20","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","reference":[{"issue":"2","key":"146976_CR1","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P. B. Andrews","year":"1981","unstructured":"Andrews, P. B.: Theorem proving via general matings, J. Association for Computing Machinery\n28(2) (1981), 193\u2013214.","journal-title":"J. Association for Computing Machinery"},{"key":"146976_CR2","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1007\/BF00881838","volume":"10","author":"A. Avron","year":"1993","unstructured":"Avron, A.: Gentzen-type systems, resolution and tableaux, J. Automated Reasoning\n10 (1993), 256\u2013281.","journal-title":"J. Automated Reasoning"},{"key":"146976_CR3","series-title":"LNAI","first-page":"462","volume-title":"11th Int. Conf. on Automated Deduction","author":"L. Bachmair","year":"1992","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C. and Snyder, W.: Basic paramodulation and superposition, in D. Kapur (ed.), 11th Int. Conf. on Automated Deduction, LNAI 607, Springer-Verlag, Saratoga Springs, NY, U.S.A., 1992, pp. 462\u2013476."},{"key":"146976_CR4","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1006\/inco.1995.1131","volume":"121","author":"L. Bachmair","year":"1995","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C. and Snyder, W.: Basic paramodulation, Information and Computation\n121 (1995), 172\u2013192.","journal-title":"Information and Computation"},{"doi-asserted-by":"crossref","unstructured":"Baumgartner, P.: An ordered theory resolution calculus, in A. Voronkov (ed.), Logic Programming and Automated Reasoning (LPAR'92), Lecture Notes in Computer Science 624, 1992, pp. 119\u2013130.","key":"146976_CR5","DOI":"10.1007\/BFb0013054"},{"key":"146976_CR6","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1006\/jsco.1993.1058","volume":"16","author":"P. Baumgartner","year":"1993","unstructured":"Baumgartner, P. and Furbach, U.: Consolution as a framework for comparing calculi, J. Symbolic Computations\n16 (1993), 445\u2013477.","journal-title":"J. Symbolic Computations"},{"doi-asserted-by":"crossref","unstructured":"Baumgartner, P. and Furbach, U.: PROTEIN: A PROver with a Theory Extension INterface, in A. Bundy (ed.), Automated Deduction \u2013 CADE-12. 12th Int. Conf. on Automated Deduction, LNAI 814, Nancy, France, 1994, pp. 769\u2013773.","key":"146976_CR7","DOI":"10.1007\/3-540-58156-1_57"},{"key":"146976_CR8","series-title":"LNAI","first-page":"319","volume-title":"KI-94: Advances in Artificial Intelligence. 18th German Annual Conference on Artificial Intelligence","author":"G. Becher","year":"1994","unstructured":"Becher, G. and Petermann, U.: Rigid unification by completion and rigid paramodulation, in B. Nebel and L. Dreschler-Fischer (eds), KI-94: Advances in Artificial Intelligence. 18th German Annual Conference on Artificial Intelligence, LNAI 861, Springer-Verlag, Saarbr\u00fccken, Germany, 1994, pp, 319\u2013330."},{"doi-asserted-by":"crossref","unstructured":"Beckert, B.: A completion-based method for mixed universal and rigid E-unification, in A. Bundy (ed.), Automated Deduction \u2013 CADE-12. 12th International Conference on Automated Deduction., LNAI 814, 678\u2013692, Nancy, France, 1994, pp. 678\u2013692.","key":"146976_CR9","DOI":"10.1007\/3-540-58156-1_49"},{"unstructured":"Beckert, B.: Are minimal solutions to simultaneous rigid E-unification sufficient for adding equality to semantic tableaux? Privately circulated manuscript, University of Karlsruhe, 1995.","key":"146976_CR10"},{"key":"146976_CR11","series-title":"LNAI","first-page":"678","volume-title":"11th International Conference on Automated Deduction (CADE)","author":"B. Beckert","year":"1992","unstructured":"Beckert, B. and H\u00e4hnle, R.: An improved method for adding equality to free variable semantic tableaux, in D. Kapur (ed.), 11th International Conference on Automated Deduction (CADE), LNAI 607, Springer-Verlag, Saratoga Springs, NY, U.S.A., 1992, pp. 678\u2013692."},{"issue":"4","key":"146976_CR12","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1145\/322276.322277","volume":"28","author":"W. Bibel","year":"1981","unstructured":"Bibel, W.: On matrices with connections, J. Association for Computing Machinery\n28(4) (1981), 633\u2013645.","journal-title":"J. Association for Computing Machinery"},{"key":"146976_CR13","series-title":"LNAI","first-page":"1","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"W. Bibel","year":"1995","unstructured":"Bibel, W., Br\u00fc:uning, S., Egly, U., Korn, D. and Rath, T.: Issues in theorem proving based on the connection method, in P. Baumgartner, R. H\u00e4hnle, and J. Posegga (eds), Theorem Proving with Analytic Tableaux and Related Methods, LNAI No. 918, Schlo\u00df Rheinfels, St. Goar, Germany, 1995, pp. 1\u201316."},{"key":"146976_CR14","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"Brand, D.: Proving theorems with the modification method, SIAM J. Computing\n4 (1975), 412\u2013430.","journal-title":"SIAM J. Computing"},{"key":"146976_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":"Chang, C. L.: Theorem proving with variable-constrained resolution, Information Sciences\n4 (1972), 217\u2013231.","journal-title":"Information Sciences"},{"key":"146976_CR16","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/3-540-59338-1_25","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"E. de Kogel","year":"1995","unstructured":"de Kogel, E.: Rigid E-unification simplified, in P. Baumgartner, R. H\u00e4hnle, and J. Posegga (eds), Theorem Proving with Analytic Tableaux and Related Methods, LNAI No. 918, Schlo\u00df Rheinfels, St. Goar, Germany, 1995, pp. 17\u201330."},{"unstructured":"Degtyarev, A. and Voronkov, A.: Equality elimination for semantic tableaux, UPMAIL Technical Report 90, Uppsala University, Computing Science Department, December 1994.","key":"146976_CR17"},{"unstructured":"Degtyarev, A. and Voronkov, A.: Equality elimination for the inverse method and extension procedures, in C. S. Mellish (ed.), Proc. International Joint Conference on Artificial Intelligence (IJCAI), Vol. 1, Montr\u00e9al, 1995, pp. 342\u2013347.","key":"146976_CR18"},{"unstructured":"Degtyarev, A. and Voronkov, A.: General connections via equality elimination, in M. De Glas and Z. Pawlak (eds), Second World Conference on the Fundamentals of Artificial Intelligence (WOCFAI-95), Angkor, Paris, 1995, pp. 109\u2013120.","key":"146976_CR19"},{"key":"146976_CR20","first-page":"503","volume-title":"Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS'96)","author":"A. Degtyarev","year":"1996","unstructured":"Degtyarev, A. and Voronkov, A.: Decidability problems for the prenex fragment of intuitionistic logic, in Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS'96), IEEE Computer Society Press, New Brunswick, NJ, 1996, pp. 503\u2013512."},{"doi-asserted-by":"crossref","unstructured":"Degtyarev, A. and Voronkov, A.: Equality elimination for the tableau method, in J. Calmet and C. Limongelli (eds), Design and Implementation of Symbolic Computation Systems. International Symposium, DISCO'96, Lecture Notes in Computer Science 1128, Karlsruhe, Germany, 1996, pp. 46\u201360.","key":"146976_CR21","DOI":"10.1007\/3-540-61697-7_4"},{"doi-asserted-by":"crossref","unstructured":"Degtyarev, A. and Voronkov, A.: Handling equality in logic programs via basic folding, in R. Dyckhoff, H. Herre, and P. Schroeder-Heister (eds), Extensions of Logic Programming (5th International Workshop, ELP'96), Lecture Notes in Computer Science 1050, Leipzig, Germany, 1996, pp. 119\u2013136.","key":"146976_CR22","DOI":"10.1007\/3-540-60983-0_8"},{"doi-asserted-by":"crossref","unstructured":"Degtyarev, A. and Voronkov, A.: Simultaneous rigid E-unification is undecidable, in H. Kleine B\u00fcning (ed.), Computer Science Logic. 9th International Workshop, CSL'95, Lecture Notes in Computer Science 1092, Paderborn, Germany, 1995, 1996, pp. 178\u2013190.","key":"146976_CR23","DOI":"10.1007\/3-540-61377-3_38"},{"issue":"1\u20132","key":"146976_CR24","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(96)00092-8","volume":"166","author":"A. Degtyarev","year":"1996","unstructured":"Degtyarev, A. and Voronkov, A.: The undecidability of simultaneous rigid E-unification, Theoretical Computer Science\n166(1\u20132) (1996), 291\u2013300.","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"Degtyarev, A. and Voronkov, A.: What you always wanted to know about rigid E-unification, in J. J. Alferes, L. M. Pereira and E. Orlowska (eds), Logics in Artificial Intelligence. European Workshop, JELIA'96, LNAI 1126, \u00c9vora, Portugal, 1996, pp. 50\u201369.","key":"146976_CR25","DOI":"10.1007\/3-540-61630-6_4"},{"unstructured":"Degtyarev, A. and Voronkov, A.: Equality reasoning and sequent-based methods, in A. Robinson and A. Voronkov (eds), Handbook of Automated Reasoning, Elsevier Science, 1998, to appear.","key":"146976_CR26"},{"key":"146976_CR27","first-page":"78","volume":"60","author":"A. Degtyarev","year":"1996","unstructured":"Degtyarev, A., Gurevich, Yu. and Voronkov, A.: Herbrand's theorem and equational reasoning: Problems and solutions, in Bulletin of the European Association for Theoretical Computer Science, The 'Logic in Computer Science' column, Vol. 60, 1996, pp. 78\u201395.","journal-title":"Bulletin of the European Association for Theoretical Computer Science"},{"key":"146976_CR28","first-page":"494","volume-title":"Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS'96)","author":"A. Degtyarev","year":"1996","unstructured":"Degtyarev, A., Matiyasevich, Yu. and Voronkov, A.: Simultaneous rigid E-unification and related algorithmic problems, in Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS'96), IEEE Computer Society Press, New Brunswick, NJ, 1996, pp. 494\u2013502."},{"key":"146976_CR29","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N.: Orderings for term rewriting systems, Theoretical Computer Science\n17 (1982), 279\u2013301.","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"Eder, E.: 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 (eds), CSL'88 (Proc. 2nd Workshop on Computer Science Logic), Lecture Notes in Computer Science 385, Springer-Verlag, 1988, pp. 80\u201398.","key":"146976_CR30","DOI":"10.1007\/BFb0026296"},{"unstructured":"Eder, E.: Consolution and its relation with resolution, in Proc. International Joint Conference on Artificial Intelligence (IJCAI), 1991, pp. 132\u2013136.","key":"146976_CR31"},{"key":"146976_CR32","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":"Fitting, M.: First Order Logic and Automated Theorem Proving, Springer-Verlag, New York, 1990."},{"unstructured":"Gallier, J. H., Raatz S. and Snyder, W.: Theorem proving using rigid E-unification: Equational matings, in Proc. IEEE Conference on Logic in Computer Science (LICS), IEEE Computer Society Press, 1987, pp. 338\u2013346.","key":"146976_CR33"},{"doi-asserted-by":"crossref","unstructured":"Gallier, J. H., Raatz, S. and Snyder, W.: Rigid E-unification and its applications to equational matings, in H. A\u00eft Kaci and M. Nivat (eds), Resolution of Equations in Algebraic Structures Vol. 1, Academic Press, 1989, pp. 151\u2013216.","key":"146976_CR34","DOI":"10.1016\/B978-0-12-046370-1.50011-5"},{"unstructured":"Gallier, J. H., Narendran, P., Plaisted, D. and Snyder, W.: Rigid E-unification is NP-complete, in Proc. IEEE Conference on Logic in Computer Science (LICS), IEEE Computer Society Press, 1988, pp. 338\u2013346.","key":"146976_CR35"},{"issue":"1\/2","key":"146976_CR36","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/0890-5401(90)90061-L","volume":"87","author":"J. Gallier","year":"1990","unstructured":"Gallier, J., Narendran, P., Plaisted, D. and Snyder, W.: Rigid E-unification: NP-completeness and applications to equational matings, Information and Computation\n87(1\/2) (1990), 129\u2013195.","journal-title":"Information and Computation"},{"issue":"2","key":"146976_CR37","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1145\/128749.128754","volume":"39","author":"J. Gallier","year":"1992","unstructured":"Gallier, J., Narendran, P., Raatz, S. and Snyder, W.: Theorem proving using equational matings and rigid E-unification, J. the Association for Computing Machinery\n39(2) (1992), 377\u2013429.","journal-title":"J. the Association for Computing Machinery"},{"doi-asserted-by":"crossref","unstructured":"Goubault, J.: A rule-based algorithm for rigid E-unification, in G. Gottlob, A. Leitsch and D. Mundici (eds), Computational Logic and Proof Theory. Proceedings of the Third Kurt G\u00f6del Colloquium, KGC'93, Lecture Notes in Computer Science 713, Brno, 1993, pp. 202\u2013210.","key":"146976_CR38","DOI":"10.1007\/BFb0022569"},{"unstructured":"Goubault, J.: Rigid E-unifiability is DEXPTIME-complete, in Proc. IEEE Conference on Logic in Computer Science (LICS), IEEE Computer Society Press, 1994.","key":"146976_CR39"},{"unstructured":"H\u00e4hnle, R., Beckert, B. and Gerberding, S.: The many-valued tableau-based theorem prover 3\nT\nAP, Technical Report 30\/94, Universit\u00e4t Karlsruhe, Fakult\u00e4t f\u00fcr Informatik, 1994.","key":"146976_CR40"},{"doi-asserted-by":"crossref","unstructured":"Kanger, S.: A simplified proof method for elementary logic, in J. Siekmann and G. Wrightson (eds), Automation of Reasoning. Classical Papers on Computational Logic, Vol. 1, Springer Verlag, 1983, pp. 364\u2013371, originally appeared in 1963.","key":"146976_CR41","DOI":"10.1007\/978-3-642-81952-0_23"},{"key":"146976_CR42","first-page":"210","volume":"95","author":"J. Kruskal","year":"1960","unstructured":"Kruskal, J.: Well quasi ordering, the tree problem and Vazsonyi's conjecture, Trans. Amer. Math. Soc.\n95 (1960), 210\u2013225.","journal-title":"Trans. Amer. Math. Soc."},{"unstructured":"Lee, R. C. T. and Chang, C. L.: Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973.","key":"146976_CR43"},{"unstructured":"Loveland, D. W.: Automated Theorem Proving: A Logical Basis, North Holland, 1978.","key":"146976_CR44"},{"key":"146976_CR45","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1007\/3-540-17220-3_4","volume":"256","author":"U. Martin","year":"1987","unstructured":"Martin, U.: How to choose weights in the Knuth-Bendix ordering, in Rewriting Technics and Applications, Lecture Notes in Computer Science 256, 1987, pp. 42\u201353.","journal-title":"Rewriting Technics and Applications"},{"key":"146976_CR46","first-page":"96","volume":"4","author":"S. Y. Maslov","year":"1967","unstructured":"Maslov, S. Yu.: Invertible sequential variant of constructive predicate calculus (in Russian), Zapiski Nauchnyh Seminarov LOMI\n4 (1967), 96\u2013111. English translation in Seminars in Mathematics: Steklov Math. Inst.\n4, Consultants Bureau, New York, London, 1969, pp. 36\u201342.","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"key":"146976_CR47","first-page":"768","volume":"148","author":"V. A. Matulis","year":"1963","unstructured":"Matulis, V. A.: On variants of classical predicate calculus with the unique deduction tree (in Russian), Soviet Math. Dokl.\n148 (1963), 768\u2013770.","journal-title":"Soviet Math. Dokl."},{"doi-asserted-by":"crossref","unstructured":"Mints, G.: Gentzen-type systems and resolution rules. Part I, Propositional logic, in P. Martin-L\u00f6f and G. Mints (eds), COLOG-88, Lecture Notes in Computer Science 417, Springer-Verlag, 1990, pp. 198\u2013231.","key":"146976_CR48","DOI":"10.1007\/3-540-52335-9_55"},{"key":"146976_CR49","series-title":"Technical Report","volume-title":"Model elimination with basic ordered paramodulation","author":"M. Moser","year":"1995","unstructured":"Moser, M., Lynch, C. and Steinbach, J.: Model elimination with basic ordered paramodulation, Technical Report AR\u201395-11, Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen, 1995."},{"key":"146976_CR50","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/0020-0190(93)90226-Y","volume":"47","author":"R. Nieuwenhuis","year":"1993","unstructured":"Nieuwenhuis, R.: Simple LPO constraint solving methods, Information Processing Letters\n47 (1993), 65\u201369.","journal-title":"Information Processing Letters"},{"doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R. and Rubio, A.: Basic superposition is complete, in ESOP'92, Lecture Notes in Computer Science 582, Springer-Verlag, 1992, pp. 371\u2013389.","key":"146976_CR51","DOI":"10.1007\/3-540-55253-7_22"},{"key":"146976_CR52","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1006\/jsco.1995.1020","volume":"19","author":"R. Nieuwenhuis","year":"1995","unstructured":"Nieuwenhuis, R. and Rubio, A.: Theorem proving with ordering and equality constrained clauses, J. Symbolic Computations\n19 (1995), 321\u2013351.","journal-title":"J. Symbolic Computations"},{"key":"146976_CR53","volume-title":"The Theory of Logical Inference","author":"S. A. Norgela","year":"1974","unstructured":"Norgela, S. A.: On the size of derivations under minus-normalization in Russian, in V. A. Smirnov (ed.), The Theory of Logical Inference, Institute of Philosophy, Moscow, 1974."},{"doi-asserted-by":"crossref","unstructured":"Petermann, U.: A complete connection calculus with rigid E-unification, in JELIA'94, Lecture Notes in Computer Science 838, 1994, pp. 152\u2013166.","key":"146976_CR54","DOI":"10.1007\/BFb0021970"},{"doi-asserted-by":"crossref","unstructured":"Plaisted, D. A.: A simple non-termination test for the Knuth-Bendix method, in Proc. 8th CADE, Lecture Notes in Computer Science 230, 1986, pp. 79\u201388.","key":"146976_CR55","DOI":"10.1007\/3-540-16780-3_81"},{"unstructured":"Plaisted, D. A.: Special cases and substitutes for rigid E-unification, Technical Report MPI-I\u201395-2-010, Max-Planck-Institut f\u00fcr Informatik, 1995.","key":"146976_CR56"},{"doi-asserted-by":"crossref","unstructured":"Prawitz, D.: An improved proof procedure, in J. Siekmann and G. Wrightson (eds), Automation of Reasoning. Classical Papers on Computational Logic, Vol. 1, Springer-Verlag, 1983, pp. 162\u2013201, originally appeared in 1960.","key":"146976_CR57","DOI":"10.1007\/978-3-642-81952-0_12"},{"unstructured":"Robinson, G. and Wos, L.: Paramodulation and theorem-proving in first order theories with equality, in B. Meltzer and D. Michie (eds), Machine Intelligence, Vol. 4, Edinburgh University Press, 1969, pp. 135\u2013150.","key":"146976_CR58"},{"issue":"3","key":"146976_CR59","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/BF00881952","volume":"13","author":"J. Schumann","year":"1994","unstructured":"Schumann, J.: Tableau-based theorem provers: Systems and implementations, J. Automated Reasoning\n13(3) (1994), 409\u2013421.","journal-title":"J. Automated Reasoning"},{"key":"146976_CR60","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1145\/359545.359570","volume":"21","author":"R. Shostak","year":"1978","unstructured":"Shostak, R.: An algorithm for reasoning about equality, Communications of the ACM\n21 (1978), 583\u2013585.","journal-title":"Communications of the ACM"},{"doi-asserted-by":"crossref","unstructured":"Smullyan, R. M.: First-Order Logic, Springer-Verlag, 1968.","key":"146976_CR61","DOI":"10.1007\/978-3-642-86718-7"},{"unstructured":"Veanes, M.: On Simultaneous Rigid E-Unification, PhD thesis, Uppsala University, 1997.","key":"146976_CR62"},{"doi-asserted-by":"crossref","unstructured":"Voronkov, A.: Proof search in intuitionistic logic with equality, or back to simultaneous rigid E-unification, in M. A. McRobbie and J. K. Slaney (eds), Automated Deduction \u2013 CADE-13, Lecture Notes in Computer Science 1104, New Brunswick, NJ, U.S.A., 1996, pp. 32\u201346. An extended version will appear in Journal of Automated Reasoning.","key":"146976_CR63","DOI":"10.1007\/3-540-61511-3_67"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005996623714.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005996623714\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005996623714.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:27:02Z","timestamp":1749122822000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005996623714"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,4]]},"references-count":63,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1998,4]]}},"alternative-id":["146976"],"URL":"https:\/\/doi.org\/10.1023\/a:1005996623714","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1998,4]]}}}