{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:10:02Z","timestamp":1749125402387,"version":"3.41.0"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1998,10,1]],"date-time":"1998-10-01T00:00:00Z","timestamp":907200000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,10,1]],"date-time":"1998-10-01T00:00:00Z","timestamp":907200000000},"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,10]]},"DOI":"10.1023\/a:1005934721802","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T00:10:48Z","timestamp":1040515848000},"page":"205-231","source":"Crossref","is-referenced-by-count":4,"title":["Proof Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification"],"prefix":"10.1007","volume":"21","author":[{"given":"Andrei","family":"Voronkov","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"149352_CR1","unstructured":"Buss, S.: Bounded Arithmetic, Vol. 3 of Studies in Proof Theory, Bibliopolis, Napoly, 1986."},{"key":"149352_CR2","doi-asserted-by":"crossref","unstructured":"Degtyarev, A., Matiyasevich, Y. and Voronkov, A.: Simultaneous rigid E-unification and related algorithmic problems, in Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS' 96), New Brunswick, NJ, 1996, pp. 494\u2013502.","DOI":"10.1109\/LICS.1996.561466"},{"key":"149352_CR3","unstructured":"Degtyarev, A. and Voronkov, A.: Equality elimination for the inverse method and extension procedures, in C. Mellish (ed.), Proc. International Joint Conference on Artificial Intelligence (IJCAI), Vol. 1, Montreal, 1995, pp. 342\u2013347."},{"key":"149352_CR4","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), Paris, 1995, pp. 109\u2013120."},{"key":"149352_CR5","doi-asserted-by":"crossref","unstructured":"Degtyarev, A. and Voronkov, A.: A new procedural interpretation of Horn clauses with equality, in L. Sterling (ed.), Proceedings of the Twelfth International Conference on Logic Programming, 1995, pp. 565\u2013579.","DOI":"10.7551\/mitpress\/4298.003.0057"},{"key":"149352_CR6","doi-asserted-by":"crossref","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), New Brunswick, NJ, 1996, pp. 503\u2013512.","DOI":"10.1109\/LICS.1996.561467"},{"key":"149352_CR7","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.","DOI":"10.1007\/3-540-61697-7_4"},{"key":"149352_CR8","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, 1996, pp. 178\u2013190.","DOI":"10.1007\/3-540-61377-3_38"},{"issue":"1\u20132","key":"149352_CR9","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"},{"key":"149352_CR10","doi-asserted-by":"crossref","unstructured":"Degtyarev, A. and Voronkov, A.: What you always wanted to know about rigid E-unification, in J. Alferes, L. Pereira and E. Orlowska (eds), Logics in Artificial Intelligence. European Workshop, JELIA' 96, Lecture Notes in Artificial Intelligence 1126, \u00c9vora, Portugal, 1996, pp. 50\u201369.","DOI":"10.1007\/3-540-61630-6_4"},{"key":"149352_CR11","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."},{"key":"149352_CR12","unstructured":"Gallier, J., Raatz, S. and Snyder, W.: Theorem proving using rigid E-unification: equational matings, in Proc. IEEE Conference on Logic in Computer Science (LICS), 1987, pp. 338\u2013346."},{"key":"149352_CR13","doi-asserted-by":"crossref","unstructured":"Garson, J.: Quantification in modal logic, in D. Gabbay and F. Guenther (eds), Handbook in Philosophical Logic, Vol. II, Chapt. II.5, D. Reidel Publishing Company, 1984, pp. 249\u2013307.","DOI":"10.1007\/978-94-009-6259-0_5"},{"key":"149352_CR14","unstructured":"Girard, J.-Y.: Proof Theory and Logical Complexity, Studies in Proof Theory, Bibliopolis, Napoly, 1987."},{"key":"149352_CR15","unstructured":"Gurevich, Y. and Veanes, M.: Some Undecidable Problems Related to the Herbrand Theorem, UPMAIL Technical Report 138, Uppsala University, Computing Science Department, 1997."},{"key":"149352_CR16","doi-asserted-by":"crossref","unstructured":"Gurevich, Y. and Voronkov, A.: Monadic simultaneous rigid E-unification and related problems, in P. Degano, R. Corrieri and A. Marchetti-Spaccamella (eds), Automata, Languages and Programming. 24th International Colloquium, ICALP' 97, Bologna, Italy, Lecture Notes in Computer Science 1256, 1997, pp. 154\u2013165.","DOI":"10.1007\/3-540-63165-8_173"},{"key":"149352_CR17","volume-title":"Provability in Logic, Vol. 1 of Studies in Philosophy","author":"S. Kanger","year":"1957","unstructured":"Kanger, S.: Provability in Logic, Vol. 1 of Studies in Philosophy, Almqvist and Wicksell, Stockholm, 1957."},{"key":"149352_CR18","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.","DOI":"10.1007\/978-3-642-81952-0_23"},{"key":"149352_CR19","unstructured":"Lee, R. and Chang, C.: Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973."},{"key":"149352_CR20","first-page":"78","volume":"4","author":"V. Lifschitz","year":"1967","unstructured":"Lifschitz, V.: Problem of decidability for some constructive theories of equalities (in Russian), Zapiski Nauchnyh Seminarov LOMI\n4 (1967), 78\u201385. English Translation in: Seminars in Mathematics: Steklov Math. Inst. 4, Consultants Bureau, New York\u2013London, 1969, pp. 29\u201331.","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"key":"149352_CR21","first-page":"5","volume":"98","author":"V. Lifschitz","year":"1968","unstructured":"Lifschitz, V.: Specialized forms of derivation in predicate calculus with equality and functional symbols (in Russian), in Trudy MIAN, Vol. 98, 1968, pp. 5\u201325. English translation in: Proc. Steklov Institute of Math., AMS, Providence, RI, 1971.","journal-title":"Trudy MIAN"},{"key":"149352_CR22","doi-asserted-by":"crossref","unstructured":"Lincoln, P. and Shankar, N.: Proof search in first-order linear logic and other cut-free sequent calculi, in S. Abramski (ed.), Ninth Annual Symposium on Logic in Computer Science, Paris, 1994, pp. 282\u2013291.","DOI":"10.1109\/LICS.1994.316061"},{"key":"149352_CR23","unstructured":"Loveland, D.: Automated Theorem Proving: A Logical Basis, North-Holland, 1978."},{"key":"149352_CR24","first-page":"96","volume":"4","author":"S. Maslov","year":"1967","unstructured":"Maslov, S.: 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. 4, Consultants Bureau, New York\u2013London, 1969, pp. 36\u201342.","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"key":"149352_CR25","doi-asserted-by":"crossref","unstructured":"Maslov, S.: An inverse method for establishing deducibility of nonprenex formulas of the predicate calculus, in J. Siekmann and G. Wrightson (eds), Automation of Reasoning (Classical papers on Computational Logic), Vol. 2, Springer-Verlag, 1983, pp. 48\u201354.","DOI":"10.1007\/978-3-642-81955-1_3"},{"key":"149352_CR26","first-page":"768","volume":"148","author":"V. Matulis","year":"1963","unstructured":"Matulis, V.: On variants of classical predicate calculus with the unique deduction tree (in Russian), Soviet Mathematical Doklady\n148 (1963), 768\u2013770.","journal-title":"Soviet Mathematical Doklady"},{"key":"149352_CR27","first-page":"78","volume":"4","author":"G. Mints","year":"1967","unstructured":"Mints, G.: Choice of terms in quantifier rules of constructive predicate calculus (in Russian), Zapiski Nauchnyh Seminarov LOMI\n4 (1967), 78\u201385. English translation in: Seminars in Mathematics: Steklov Math. Inst. 4, Consultants Bureau, New York\u2013London, 1969, pp. 43\u201346.","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"key":"149352_CR28","first-page":"110","volume":"32","author":"V. Orevkov","year":"1974","unstructured":"Orevkov, V.: A specialized form of derivation in gentzen calculi and its applications (in Russian), Zapiski Nauchnyh Seminarov LOMI\n32 (1974), 110\u2013118.","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"key":"149352_CR29","first-page":"109","volume":"60","author":"V. Orevkov","year":"1976","unstructured":"Orevkov, V.: Solvable classes of pseudo-prenex formulas (in Russian), Zapiski Nauchnyh Seminarov LOMI\n60 (1976), 109\u2013170. English translation in: Journal of Soviet Mathematics.","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"key":"149352_CR30","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.","DOI":"10.1007\/BFb0021970"},{"key":"149352_CR31","unstructured":"Plaisted, D.: Special Cases and Substitutes for Rigid E-Unification, Technical Report MPI-I-95-2-10, Max-Planck-Institut f\u00fcr Informatik, 1995."},{"key":"149352_CR32","unstructured":"Plotkin, G.: Building-in equational theories, in B. Meltzer and D. Michie (eds), Machine Intelligence, Vol. 7, Edinburgh University Press, 1972, pp. 73\u201390."},{"key":"149352_CR33","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."},{"issue":"1","key":"149352_CR34","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. Robinson","year":"1965","unstructured":"Robinson, J.: A machine-oriented logic based on the resolution principle, Journal of the Association for Computing Machinery\n12(1) (1965), 23\u201341.RSMS23.tex; 19\/08\/1998; 8:51; v.7; p.26","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"5","key":"149352_CR35","doi-asserted-by":"crossref","first-page":"619","DOI":"10.1093\/logcom\/2.5.619","volume":"2","author":"D. Sahlin","year":"1992","unstructured":"Sahlin, D., Franz\u00e9n, T. and Haridi, S.: An intuitionistic predicate logic theorem prover, Journal of Logic and Computation\n2(5) (1992), 619\u2013656.","journal-title":"Journal of Logic and Computation"},{"key":"149352_CR36","doi-asserted-by":"crossref","unstructured":"Sazonov, V.: A logical approach to the problem \u201cP = NP?\u201d, in Mathematical Foundations of Computer Science, Lecture Notes in Computer Science 88, 1980, pp. 562\u2013575.","DOI":"10.1007\/BFb0022533"},{"key":"149352_CR37","doi-asserted-by":"crossref","unstructured":"Shankar, N.: Proof search in the intuitionistic sequent calculus, in D. Kapur (ed.), 11th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 607, Saratoga Springs, NY, 1992, pp. 522\u2013536.","DOI":"10.1007\/3-540-55602-8_189"},{"key":"149352_CR38","doi-asserted-by":"crossref","unstructured":"Tammet, T.: A resolution theorem prover for intuitionistic logic, in M. McRobbie and J. Slaney (eds), Automated Deduction \u2014 CADE-13, Lecture Notes in Computer Science 1104, New Brunswick, NJ, 1996, pp. 2\u201316.","DOI":"10.1007\/3-540-61511-3_65"},{"key":"149352_CR39","unstructured":"Veanes, M.: Uniform Representation of Recursively Enumerable Sets with Simultaneous Rigid E-Unification, UPMAIL Technical Report 126, Uppsala University, Computing Science Department, 1996."},{"key":"149352_CR40","unstructured":"Veanes, M.: On Simultaneous Rigid E-Unification, Ph.D. thesis, Uppsala University, 1997."},{"key":"149352_CR41","unstructured":"Voda, P. and Komara, J.: On Herbrand Skeletons, Technical Report, Institute of Informatics, Comenius University Bratislava, 1995."},{"key":"149352_CR42","doi-asserted-by":"crossref","unstructured":"Voronkov, A.: Theorem proving in non-standard logics based on the inverse method, in D. Kapur (ed.), 11th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 607, Saratoga Springs, NY, USA, 1992, pp. 648\u2013662.","DOI":"10.1007\/3-540-55602-8_198"},{"key":"149352_CR43","doi-asserted-by":"crossref","unstructured":"Voronkov, A.: Proof search in intuitionistic logic based on constraint satisfaction, in P. Miglioli, U. Moscato, D. Mundici and M. Ornaghi (eds), Theorem Proving with Analytic Tableaux and Related Methods. 5th International Workshop, TABLEAUX' 96, Terrasini, Palermo, Italy, Lecture Notes in Artificial Intelligence 1071, 1996, pp. 312\u2013329.","DOI":"10.1007\/3-540-61208-4_20"},{"key":"149352_CR44","doi-asserted-by":"crossref","unstructured":"Voronkov, A.: Proof search in intuitionistic logic with equality, or back to simultaneous rigid E-unification, in M. McRobbie and J. Slaney (eds), Automated Deduction \u2014 CADE-13, Lecture Notes in Computer Science 1104, New Brunswick, NJ, USA, 1996, pp. 32\u201346.","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:1005934721802.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005934721802\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005934721802.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:45:36Z","timestamp":1749123936000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005934721802"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,10]]},"references-count":44,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1998,10]]}},"alternative-id":["149352"],"URL":"https:\/\/doi.org\/10.1023\/a:1005934721802","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1998,10]]}}}