{"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":1749125181887},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615118"},{"type":"electronic","value":"9783540686873"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61511-3_67","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:50:23Z","timestamp":1330293023000},"page":"32-46","source":"Crossref","is-referenced-by-count":12,"title":["Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification"],"prefix":"10.1007","author":[{"given":"Andrei","family":"Voronkov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"key":"4_CR1","first-page":"15","volume":"60","author":"A. Beltyukov","year":"1976","unstructured":"A. Beltyukov. Decidability of the universal theory of natural numbers with addition and divisibility (in Russian). Zapiski Nauchnyh Seminarov LOMI, 60:15\u201328, 1976. English translation in: Journal of Soviet Mathematics.","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"key":"4_CR2","unstructured":"A. Degtyarev, Yu. Matiyasevich, and A. Voronkov. Simultaneous rigid E-unification and related algorithmic problems. In LICS'96, page 11, 1996."},{"key":"4_CR3","unstructured":"A. Degtyarev and A. Voronkov. Equality elimination for semantic tableaux. UP-MAIL Technical Report 90, Uppsala University, Computing Science Department, December 1994."},{"key":"4_CR4","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.","DOI":"10.1007\/3-540-61377-3_38"},{"key":"4_CR5","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_CR6","doi-asserted-by":"crossref","unstructured":"A. Degtyarev and A. Voronkov. A new procedural interpretation of Horn clauses with equality. In Leon Sterling, editor, Proceedings of the Twelfth International Conference on Logic Programming, pages 565\u2013579. The MIT Press, 1995.","DOI":"10.7551\/mitpress\/4298.003.0057"},{"key":"4_CR7","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_CR8","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_CR9","unstructured":"A. Degtyarev and A. Voronkov. Skolemization and decidability problems for fragments of intuitionistic logic. Submitted, 10 pages, 1996."},{"key":"4_CR10","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."},{"key":"4_CR11","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_CR12","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_CR13","unstructured":"R.C.T. Lee and C.L. Chang. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973."},{"key":"4_CR14","first-page":"78","volume":"4","author":"V. Lifschitz","year":"1967","unstructured":"V. Lifschitz. The decidability problem for some constructive theories of equality (in Russian). Zapiski Nauchnyh Seminarov LOMI, 4:78\u201385, 1967.","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"key":"4_CR15","unstructured":"D.W. Loveland. Automated Theorem Proving: a Logical Basis. North Holland, 1978."},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"S.Yu. Maslov. An inverse method for establishing deducibility of nonprenex formulas of the predicate calculus. In J.Siekmann and G.Wrightson, editors, Automation of Reasoning (Classical papers on Computational Logic), volume 2, pages 48\u201354. Springer Verlag, 1983.","DOI":"10.1007\/978-3-642-81955-1_3"},{"key":"4_CR17","doi-asserted-by":"crossref","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.","DOI":"10.1007\/978-1-4684-8968-2_10"},{"key":"4_CR18","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_CR19","first-page":"78","volume":"4","author":"G.E. Mints","year":"1967","unstructured":"G.E. Mints. Collecting terms in the quantifier rules of the constructive predicate calculus (in Russian). Zapiski Nauchnyh Seminarov LOMI, 4:78\u201385, 1967.","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"key":"4_CR20","first-page":"109","volume":"60","author":"V.P. Orevkov","year":"1976","unstructured":"V.P. Orevkov. Solvable classes of pseudo-prenex formulas (in Russian). Zapiski Nauchnyh Seminarov LOMI, 60:109\u2013170, 1976. English translation in: Journal of Soviet Mathematics.","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"key":"4_CR21","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_CR22","first-page":"73","volume-title":"Machine Intelligence, volume 7","author":"G. Plotkin","year":"1972","unstructured":"G. Plotkin. Building-in equational theories. In Meltzer and Michie, editors, Machine Intelligence, volume 7, pages 73\u201390. Edinburgh University Press, Edinburgh, 1972."},{"key":"4_CR23","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":"5","key":"4_CR24","doi-asserted-by":"crossref","first-page":"619","DOI":"10.1093\/logcom\/2.5.619","volume":"2","author":"D. Sahlin","year":"1992","unstructured":"D. Sahlin, T. Franz\u00e9n, and S. Haridi. An intuitionistic predicate logic theorem prover. Journal of Logic and Computation, 2(5):619\u2013656, 1992.","journal-title":"Journal of Logic and Computation"},{"key":"4_CR25","first-page":"522","volume-title":"volume 607 of Lecture Notes in Artificial Intelligence","author":"N. Shankar","year":"1992","unstructured":"N. Shankar. Proof search in the intuitionistic sequent calculus. In D. Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 522\u2013536, Saratoga Springs, NY, USA, June 1992. Springer Verlag."},{"key":"4_CR26","unstructured":"T. Tammet. A resolution theorem prover for intuitionistic logic. This volume."},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"M. Veanes. Undecidability proofs of simultaneous rigid E-unification. Upmail technical report, Uppsala University, Computing Science Department, 1996. To appear.","DOI":"10.1007\/3-540-63385-5_52"},{"key":"4_CR28","unstructured":"P.J. Voda and J. Komara. On Herbrand skeletons. Technical report, Institute of Informatics, Comenius University Bratislava, July 1995."},{"key":"4_CR29","first-page":"648","volume-title":"volume 607 of Lecture Notes in Artificial Intelligence","author":"A. Voronkov","year":"1992","unstructured":"A. Voronkov. Theorem proving in non-standard logics based on the inverse method. In D. Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 648\u2013662, Saratoga Springs, NY, USA, June 1992. Springer Verlag."},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"A. Voronkov. Proof-search in intuitionistic logic based on the constraint satisfaction. UPMAIL Technical Report 120, Uppsala University, Computing Science Department, January 1996.","DOI":"10.1007\/3-540-61208-4_20"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"A. Voronkov. On proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-Unification. UPMAIL Technical Report 121, Uppsala University, Computing Science Department, January 1996.","DOI":"10.1007\/3-540-61511-3_67"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 Cade-13"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61511-3_67.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T17:33:16Z","timestamp":1713634396000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61511-3_67"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615118","9783540686873"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-61511-3_67","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}