{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:20Z","timestamp":1749125180207},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540616979"},{"type":"electronic","value":"9783540706359"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61697-7_4","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:13:28Z","timestamp":1330294408000},"page":"46-60","source":"Crossref","is-referenced-by-count":8,"title":["Equality elimination for the tableau method"],"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,3]]},"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":"crossref","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. Basic paramodulation. Information and Computation, 121:172\u2013192, 1995.","journal-title":"Information and Computation"},{"key":"4_CR3","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_CR4","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."},{"key":"4_CR5","unstructured":"E.W. Beth. The Foundations of Mathematics. North Holland, 1959."},{"issue":"4","key":"4_CR6","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_CR7","doi-asserted-by":"crossref","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"},{"issue":"3","key":"4_CR8","doi-asserted-by":"crossref","first-page":"290","DOI":"10.1007\/BF01069968","volume":"22","author":"A. Degtyarev","year":"1986","unstructured":"A. Degtyarev and A. Voronkov. Automated theorem proving I and II. Cybernetics, 22(3):290\u2013297, 1986 and 23(4):547\u2013556, 1987.","journal-title":"Cybernetics"},{"issue":"3","key":"4_CR9","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/BF01069968","volume":"22","author":"A. Degtyarev","year":"1986","unstructured":"A. Degtyarev and A. Voronkov. Equality control methods in machine theorem proving. Cybernetics, 22(3):298\u2013307, 1986.","journal-title":"Cybernetics"},{"key":"4_CR10","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_CR11","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_CR12","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_CR13","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.","DOI":"10.1016\/0304-3975(96)00092-8"},{"key":"4_CR14","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_CR15","doi-asserted-by":"crossref","unstructured":"A. Degtyarev and A. Voronkov. What you always wanted to know about rigid E-unification. In Submitted to JELIA '96, page 20, 1996.","DOI":"10.1007\/3-540-61630-6_4"},{"key":"4_CR16","unstructured":"R. Demolombe. An efficient strategy for non-Horn deductive databases. In G.X. Ritter, editor, Information Processing 89, pages 325\u2013330. Elsevier Science, 1989."},{"key":"4_CR17","series-title":"volume B: Formal Methods and Semantics","first-page":"243","volume-title":"Handbook of Theoretical Computer Science","author":"N. Dershowitz","year":"1990","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. Van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, chapter 6, pages 243\u2013309. North Holland, Amsterdam, 1990."},{"key":"4_CR18","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_CR19","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."},{"issue":"2","key":"4_CR20","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_CR21","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_CR22","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_CR23","unstructured":"R.C.T. Lee and C.L. Chang. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973."},{"key":"4_CR24","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_CR25","doi-asserted-by":"crossref","unstructured":"E.L. Lusk. Controlling redundancy in large search spaces: Argonne-style theorem proving through the years. In A. Voronkov, editor, Logic Programming and Automated Reasoning. International Conference LPAR'92., volume 624 of Lecture Notes in Artificial Intelligence, pages 96\u2013106, St.Petersburg, Russia, July 1992.","DOI":"10.1007\/BFb0013052"},{"key":"4_CR26","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_CR27","series-title":"Seminars in Mathematics: Steklov Math. Inst. 4","first-page":"36","volume-title":"Zapiski Nauchnyh Seminarov LOMI, 4, 1967","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_CR28","first-page":"80","volume":"20","author":"S. Maslov","year":"1971","unstructured":"S.Yu. Maslov. The generalization of the inverse method to predicate calculus with equality (in Russian). Zapiski Nauchnyh Seminarov LOMI, 20:80\u201396, 1971. English translation in: Journal of Soviet Mathematics 1, no. 1.","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"S.Yu. Maslov, G.E. Mints, and V.P. Orevkov. Mechanical proof-search and the theory of logical deduction in the USSR. In J.Siekmann and G.Wrightson, editors, Automation of Reasoning (Classical papers on Computational Logic), volume 1, pages 29\u201338. Springer Verlag, 1983.","DOI":"10.1007\/978-3-642-81952-0_2"},{"key":"4_CR30","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_CR31","first-page":"613","volume-title":"Computational Logic. Essays in Honor of Alan Robinson","author":"J. Minker","year":"1991","unstructured":"J. Minker, A. Rajasekar, and J. Lobo. Theory of disjunctive logic programs. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic. Essays in Honor of Alan Robinson., pages 613\u2013639. The MIT Press, Cambridge, MA, 1991."},{"key":"4_CR32","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_CR33","doi-asserted-by":"crossref","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_CR34","first-page":"152","volume":"16","author":"V.P. Orevkov","year":"1969","unstructured":"V.P. Orevkov. On nonlengthening rule applications for equality (in Russian). Zapiski Nauchnyh Seminarov LOMI, 16:152\u2013156, 1969. English Translation in: Seminars in Mathematics: Steklov Math. Inst. 16, Consultants Bureau, NY-London, 1971, p.77\u201379.","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"key":"4_CR35","doi-asserted-by":"crossref","first-page":"152","DOI":"10.1007\/BFb0021970","volume":"838","author":"U. Petermann","year":"1994","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.","journal-title":"Lecture Notes in Computer Science"},{"key":"4_CR36","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"},{"issue":"3","key":"4_CR37","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_CR38","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_CR39","doi-asserted-by":"crossref","unstructured":"R.M. Smullyan. First-Order Logic. Springer Verlag, 1968.","DOI":"10.1007\/978-3-642-86718-7"},{"key":"4_CR40","first-page":"677","volume-title":"volume 449 of Lecture Notes in Computer Science","author":"A. Voronkov","year":"1990","unstructured":"A. Voronkov. LISS \u2014 the logic inference search system. In Mark Stickel, editor, Proc. 10th Int. Conf. on Automated Deduction, volume 449 of Lecture Notes in Computer Science, pages 677\u2013678, Kaiserslautern, Germany, 1990. Springer Verlag."},{"key":"4_CR41","doi-asserted-by":"crossref","unstructured":"A. Voronkov. A proof-search method for the first order logic. In P. Martin-L\u00f6f and G. Mintz, editors, COLOG'88, volume 417 of Lecture Notes in Computer Science, pages 327\u2013340. Springer Verlag, 1990.","DOI":"10.1007\/3-540-52335-9_63"},{"key":"4_CR42","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_CR43","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1147\/rd.41.0002","volume":"4","author":"H. Wang","year":"1960","unstructured":"H. Wang. Towards mechanical mathematics. IBM J. of Research and Development, 4:2\u201322, 1960.","journal-title":"IBM J. of Research and Development"}],"container-title":["Lecture Notes in Computer Science","Design and Implementation of Symbolic Computation Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61697-7_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T17:41:45Z","timestamp":1713634905000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61697-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540616979","9783540706359"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/3-540-61697-7_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}