{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,19]],"date-time":"2025-11-19T06:48:42Z","timestamp":1763534922354},"reference-count":192,"publisher":"Elsevier","isbn-type":[{"value":"9780444508133","type":"print"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1016\/b978-044450813-3\/50012-6","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T13:04:11Z","timestamp":1181567051000},"page":"611-706","source":"Crossref","is-referenced-by-count":27,"title":["Equality Reasoning in Sequent-Based Calculi"],"prefix":"10.1016","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":"78","reference":[{"key":"10.1016\/B978-044450813-3\/50012-6_bb0010","doi-asserted-by":"crossref","first-page":"801","DOI":"10.1109\/TC.1976.1674698","article-title":"Refutations by matings","volume":"25","author":"Andrews","year":"1976","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"10.1016\/B978-044450813-3\/50012-6_bb0015","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","article-title":"Theorem proving via general matings","volume":"28","author":"Andrews","year":"1981","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0020","series-title":"An introduction to type theory: to truth through proof","author":"Andrews","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0025","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1007\/BF00881838","article-title":"Gentzen-type systems, resolution and tableaux","volume":"10","author":"Avron","year":"1993","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0030","series-title":"Arithmetic, Proof Theory and Computation Complexity","first-page":"20","article-title":"Note on the existence of most general semi-unifiers","author":"Baaz","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0035","series-title":"Theorem Proving with Analytic Tableaux and Related Methods","first-page":"217","article-title":"Non-elementary speedups between different versions of tableaux","author":"Baaz","year":"1995"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50012-6_bb0040","doi-asserted-by":"crossref","DOI":"10.3233\/FI-1994-2044","article-title":"On skolemization and proof complexity","volume":"20","author":"Baaz","year":"1994","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0045","series-title":"Proc. 10th CADE","first-page":"427","article-title":"On restriction of ordered paramodulation with simplication","author":"Bachmair","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0050","series-title":"Conditional and Typed Rewriting Systems","first-page":"164","article-title":"Completion of first-order clauses with equality by strict superposition","author":"Bachmair","year":"1991"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50012-6_bb0055","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","article-title":"Rewrite-based equational theorem proving with selection and simplification","volume":"4","author":"Bachmair","year":"1994","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0060","series-title":"Automated Deduction \u2014 CADE-15. 15th International Conference on Automated Deduction","first-page":"160","article-title":"Strict basic superposition","author":"Bachmair","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0065","series-title":"11th International Conference on Automated Deduction","first-page":"462","article-title":"Basic paramodulation and superposition","author":"Bachmair","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0070","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1006\/inco.1995.1131","article-title":"Basic paramodulation","volume":"121","author":"Bachmair","year":"1995","journal-title":"Information and Computation"},{"key":"10.1016\/B978-044450813-3\/50012-6_rf0075","series-title":"Automated Deduction \u2014 CADE-15. 15th International Conference on Automated Deduction","first-page":"175","article-title":"Elimination of equality via transformation with ordering constraints","author":"Bachmair","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0080","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1006\/jsco.1993.1058","article-title":"Consolution as a framework for comparing calculi","volume":"16","author":"Baumgartner","year":"1993","journal-title":"Journal of Symbolic Computations"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0085","series-title":"Automated Deduction \u2014 CADE-12. 12th International Conference on Automated Deduction","first-page":"769","article-title":"PROTEIN: A PROver with a Theory Extension INterface","author":"Baumgartner","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0090","series-title":"KI-94: Advances in Artificial Intelligence. 18th German Annual Conference on Artificial Intelligence","first-page":"319","article-title":"Rigid unification by completion and rigid paramodulation","author":"Becher","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0095","series-title":"Automated Deduction \u2014 CADE-12. 12th International Conference on Automated Deduction","first-page":"678","article-title":"A completion-based method for mixed universal and rigid E-unification","author":"Beckert","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0100","series-title":"Are minimal solutions to simultaneous rigid E-unification sufficient for adding equality to semantic tableaux?","author":"Beckert","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0105","series-title":"Handbook of Tableau Methods","article-title":"Equality and other theory inferences","author":"Beckert","year":"1997"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50012-6_bb0110","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1093\/logcom\/7.1.39","article-title":"Semantic tableaux with equality","volume":"7","author":"Beckert","year":"1997","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0115","series-title":"11th International Conference on Automated Deduction (CADE)","first-page":"678","article-title":"An improved method for adding equality to free variable semantic tableaux","author":"Beckert","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0120","series-title":"Computational Logic and Proof Theory. Proceedings of the Third Kurt G\u00f6del Colloquium, KGC'93","first-page":"108","article-title":"The even more liberalized \u03b4-rule in free variable semantic tableaux","author":"Beckert","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0125","first-page":"15","article-title":"Decidability of the universal theory of natural numbers with addition and divisibility","volume":"60","author":"Beltyukov","year":"1976","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0130","series-title":"Proc. 10th Int. Conf. on Automated Deduction","first-page":"442","article-title":"Simultaneous paramodulation","author":"Benanav","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0135","article-title":"The Foundations of Mathematics","author":"Beth","year":"1959"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0140","series-title":"Automation of Reasoning. Classical Papers on Computational Logic","first-page":"79","article-title":"On machines which prove theorems","author":"Beth","year":"1983"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50012-6_bb0145","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1145\/322276.322277","article-title":"On matrices with connections","volume":"28","author":"Bibel","year":"1981","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0150","series-title":"Deduction. Automated Logic.","author":"Bibel","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0155","series-title":"Theorem Proving with Analytic Tableaux and Related Methods","first-page":"1","article-title":"Issues in theorem proving based on the connection method","author":"Bibel","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0160","series-title":"Proc. Int. Computing Symp.","first-page":"205","article-title":"Proof search in a Gentzen-like system of first order logic","author":"Bibel","year":"1975"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0165","series-title":"Proc. 10th CADE","first-page":"558","article-title":"Minimizing the number of clauses by renaming","author":"Boy de la Tour","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50012-6_rf0170","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1137\/0204036","article-title":"Proving theorems with the modification method","volume":"4","author":"Brand","year":"1975","journal-title":"SIAM Journal of Computing"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0175","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/S0020-0255(72)80012-4","article-title":"Theorem proving with variable-constrained resolution","volume":"4","author":"Chang","year":"1972","journal-title":"Information Sciences"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0180","series-title":"Automata, Languages and Programming, 26th International Colloquium, ICALP'99, Prague, Czech Republic, July 11-15, 1999, Proceedings","first-page":"250","article-title":"Decidable fragments of simultaneous rigid reachability","author":"Cortier","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0185","series-title":"Foundations of Mathematical Logic","author":"Curry","year":"1963"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0190","series-title":"Machine Intelligence","first-page":"113","article-title":"Automatic theorem proving with equality substitutions and mathematical induction","author":"Darlington","year":"1968"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0195","series-title":"Theorem Proving with Analytic Tableaux and Related Methods","first-page":"17","article-title":"Rigid E-unification simplified","author":"De Kogel","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0200","series-title":"Fifth Soviet All-Union Conference on Mathematical Logic","first-page":"39","article-title":"The strategy of monotone paramodulation","author":"Degtyarev","year":"1979"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0205","series-title":"Automation of Research in Mathematics","first-page":"14","article-title":"On the forms of inference in calculi with equality and paramodulation","author":"Degtyarev","year":"1982"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0210","series-title":"Proc. of the Soviet Conf. on Applied Logic","first-page":"69","article-title":"Rewriting strategies for computational logic","author":"Degtyarev","year":"1985"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0215","article-title":"The decidability of simultaneous rigid E-unification with one variable","author":"Degtyarev","year":"1997","journal-title":"UPMAIL Technical Report 139, Uppsala University, Computing Science Department"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0220","series-title":"Rewriting Techniques and Applications, RTA'98","first-page":"181","article-title":"The decidability of simultaneous rigid E-unification with one variable","author":"Degtyarev","year":"1998"},{"issue":"1-2","key":"10.1016\/B978-044450813-3\/50012-6_bb0225","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1016\/S0304-3975(98)00185-6","article-title":"The decidability of simultaneous rigid E-unification with one variable and related results","volume":"243","author":"Degtyarev","year":"2000","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0230","first-page":"78","article-title":"Herbrand's theorem and equational reasoning: Problems and solutions","volume":"Vol. 60","author":"Degtyarev","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0235","series-title":"Logic in Computer Science","article-title":"Herbrand's theorem and equational reasoning: Problems and solutions","author":"Degtyarev","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0240","article-title":"Handling equality in logic programming via basic folding","author":"Degtyarev","year":"1995","journal-title":"UPMAIL Technical Report 101, Uppsala University, Computing Science Department"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0245","article-title":"Simultaneous rigid E-unification is not so simple","author":"Degtyarev","year":"1995","journal-title":"UPMAIL Technical Report 104, Uppsala University, Computing Science Department"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0250","series-title":"Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS'96)","first-page":"494","article-title":"Simultaneous rigid E-unification and related algorithmic problems","author":"Degtyarev","year":"1996"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50012-6_bb0255","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/BF01069968","article-title":"Equality control methods in machine theorem proving","volume":"22","author":"Degtyarev","year":"1986","journal-title":"Cybernetics"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0260","article-title":"Equality elimination for semantic tableaux","author":"Degtyarev","year":"1994","journal-title":"UPMAIL Technical Report 90, Uppsala University, Computing Science Department"},{"key":"10.1016\/B978-044450813-3\/50012-6_rf0265","article-title":"A new procedural interpretation of Horn clauses with equality","author":"Degtyarev","year":"1994","journal-title":"UPMAIL Technical Report 89, Uppsala University, Computing Science Department"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0270","series-title":"Proc. International Joint Conference on Artificial Intelligence (IJCAI)","first-page":"342","article-title":"Equality elimination for the inverse method and extension procedures","author":"Degtyarev","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0275","series-title":"Second World Conference on the Fundamentals of Artificial Intelligence (WOCFAI-95)","first-page":"109","article-title":"General connections via equality elimination","author":"Degtyarev","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0280","series-title":"Proceedings of the Twelfth International Conference on Logic Programming","first-page":"565","article-title":"A new procedural interpretation of Horn clauses with equality","author":"Degtyarev","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0285","article-title":"Reduction of second-order unification to simultaneous rigid E-unification","author":"Degtyarev","year":"1995","journal-title":"UPMAIL Technical Report 109, Uppsala University, Computing Science Department"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0290","article-title":"Simultaneous rigid E-unification is undecidable","author":"Degtyarev","year":"1995","journal-title":"UPMAIL Technical Report 105, Uppsala University, Computing Science Department"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0295","series-title":"Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS'96)","first-page":"503","article-title":"Decidability problems for the prenex fragment of intuitionistic logic","author":"Degtyarev","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0300","series-title":"Design and Implementation of Symbolic Computation Systems. International Symposium, DISCO'96","first-page":"46","article-title":"Equality elimination for the tableau method","author":"Degtyarev","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0305","series-title":"Extensions of Logic Programming (5th International Workshop, ELP'96)","first-page":"119","article-title":"Handling equality in logic programs via basic folding","author":"Degtyarev","year":"1996"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50012-6_bb0310","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/0743-1066(96)00049-0","article-title":"A note on semantics of logics programs with equality based on complete sets of E-unifiers","volume":"28","author":"Degtyarev","year":"1996","journal-title":"Journal of Logic Programming"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0315","series-title":"Computer Science Logic. 9th International Workshop, CSL'95","first-page":"178","article-title":"Simultaneous rigid E-unification is undecidable","author":"Degtyarev","year":"1995-1996"},{"issue":"1-2","key":"10.1016\/B978-044450813-3\/50012-6_bb0320","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(96)00092-8","article-title":"The undecidability of simultaneous rigid E-unification","volume":"166","author":"Degtyarev","year":"1996","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0325","series-title":"Logics in Artificial Intelligence. European Workshop, JELIA'96","first-page":"50","article-title":"What you always wanted to know about rigid E-unification","author":"Degtyarev","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0330","article-title":"What you always wanted to know about rigid E-unification","author":"Degtyarev","year":"1997","journal-title":"UPMAIL Technical Report 143, Uppsala University, Computing Science Department"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50012-6_bb0335","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1023\/A:1005996623714","article-title":"What you always wanted to know about rigid E-unification","volume":"20","author":"Degtyarev","year":"1998","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0340","first-page":"1","article-title":"Handling equality in logic programming via basic folding","author":"Degtyarev","year":"2001","journal-title":"Journal of Symbolic Computations"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0345","first-page":"179","article-title":"The inverse method","volume":"Vol. I","author":"Degtyarev","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0350","series-title":"Collected papers of Stig Kanger with Essays on his Life and Work","first-page":"1","article-title":"Kanger's choices in automated reasoning","author":"Degtyarev","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50012-6_rf0355","first-page":"1009","article-title":"Higher-order unification and matching","volume":"Vol. II","author":"Dowek","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0360","series-title":"AIMSA'84, Artificial Intelligence \u2014 Methodology, Systems, Application","first-page":"121","article-title":"An implementation of a theorem prover based on the connection method","author":"Eder","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0365","series-title":"CSL'88 (Proc. 2nd Workshop on Computer Science Logic)","first-page":"80","article-title":"A comparison of the resolution calculus and the connection method, and a new calculus generalizing both methods","author":"Eder","year":"1988"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0370","series-title":"Proc. International Joint Conference on Artificial Intelligence (IJCAI)","first-page":"132","article-title":"Consolution and its relation with resolution","author":"Eder","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0375","series-title":"First Order Logic and Automated Theorem Proving","author":"Fitting","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0380","series-title":"Computational Logic. Essays in Honor of Alan Robinson","first-page":"113","article-title":"Modal logic should say more than it does","author":"Fitting","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0385","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/BF00881954","article-title":"Tableaux for logic programming","volume":"13","author":"Fitting","year":"1994","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0390","series-title":"First Order Logic and Automated Theorem Proving","author":"Fitting","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0395","series-title":"Logic for Computer Science: Foundations of Automatic Theorem Proving","author":"Gallier","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0400","series-title":"Tree Automata and Languages","first-page":"439","article-title":"Unification procedures in automated deduction methods based on matings: a survey","author":"Gallier","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0405","series-title":"Proc. IEEE Conference on Logic in Computer Science (LICS)","first-page":"338","article-title":"Rigid E-unification is NP-complete","author":"Gallier","year":"1988"},{"issue":"1\/2","key":"10.1016\/B978-044450813-3\/50012-6_bb0410","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/0890-5401(90)90061-L","article-title":"Rigid E-unification: NP-completeness and applications to equational matings","volume":"87","author":"Gallier","year":"1990","journal-title":"Information and Computation"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50012-6_bb0415","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1145\/128749.128754","article-title":"Theorem proving using equational matings and rigid E-unification","volume":"39","author":"Gallier","year":"1992","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0420","series-title":"Proc. IEEE Conference on Logic in Computer Science (LICS)","first-page":"338","article-title":"Theorem proving using rigid E-unification: Equational matings","author":"Gallier","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0425","series-title":"Resolution of Equations in Algebraic Structures","first-page":"151","article-title":"Rigid E-unification and its applications to equational matings","author":"Gallier","year":"1989"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0430","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/0304-3975(89)90004-2","article-title":"Complete sets of transformations for general E-unification","volume":"67","author":"Gallier","year":"1989","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0435","series-title":"Advances in Computing Science - ASIAN'98, 4th Asian Computing Science Conference","first-page":"4","article-title":"Rigid reachability","author":"Ganzinger","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0440","first-page":"249","article-title":"Quantification in modal logic","volume":"Vol. II","author":"Garson","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50012-6_rf0445","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen","volume":"39","author":"Gentzen","year":"1934","journal-title":"Mathematical Zeitschrift"},{"key":"10.1016\/B978-044450813-3\/50012-6_rf0450","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/BF01201363","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen","volume":"39","author":"Gentzen","year":"1934","journal-title":"Mathematical Zeitschrift"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0450","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/BF01565428","article-title":"Die Wiederspruchsfreiheit der reinen Zahlentheorie","volume":"112","author":"Gentzen","year":"1936","journal-title":"Mathematische Annalen"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50012-6_rf0460","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear logic","volume":"50","author":"Girard","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0460","series-title":"Studies in Proof Theory","article-title":"Proof Theory and Logical Complexity","author":"Girard","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0465","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","article-title":"The undecidability of the second-order unification problem","volume":"13","author":"Goldfarb","year":"1981","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0470","series-title":"Computational Logic and Proof Theory. Proceedings of the Third Kurt G\u00f6del Colloquium, KGC'93","first-page":"202","article-title":"A rule-based algorithm for rigid E-unification","author":"Goubault","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0475","series-title":"Proc. IEEE Conference on Logic in Computer Science (LICS)","article-title":"Rigid E-unifiability is DEXPTIME-complete","author":"Goubault","year":"1994"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0480","article-title":"Monadic simultaneous rigid E-unification and related problems","author":"Gurevich","year":"1997","journal-title":"UPMAIL Technical Report 137, Uppsala University, Computing Science Department"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0485","series-title":"Automata, Languages and Programming. 24th International Colloquium, ICALP'97","first-page":"154","article-title":"Monadic simultaneous rigid E-unification and related problems","author":"Gurevich","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0490","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/S0304-3975(98)00123-6","article-title":"Monadic simultaneous rigid E-unification","volume":"222","author":"Gurevich","year":"1999","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0495","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/BF00881956","article-title":"The liberalized \u03b4-rule in free variable semantic tableaux","volume":"13","author":"H\u00e4hnle","year":"1994","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0500","series-title":"Proc. 8th CADE","first-page":"141","article-title":"A new method for establishing refutational completeness in theorem proving","author":"Hsiang","year":"1986"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50012-6_bb0505","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1145\/116825.116833","article-title":"Proving refutational completeness of theorem proving strategies: the transfinite semantic tree method","volume":"38","author":"Hsiang","year":"1991","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0510","series-title":"5th CADE","first-page":"318","article-title":"Canonical forms and unification","author":"Hullot","year":"1980"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0515","series-title":"Automated Reasoning with Analytic Tableaux and Related Methods","first-page":"201","article-title":"Subgoal alternation in model elimination","author":"Ibens","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0520","series-title":"Provability in Logic, Vol. 1 of Studies in Philosophy","author":"Kanger","year":"1957"},{"key":"10.1016\/B978-044450813-3\/50012-6_rf0530","series-title":"Computer Programming and Formal Systems","first-page":"87","article-title":"A simplified proof method for elementary logic","author":"Kanger","year":"1963"},{"key":"10.1016\/B978-044450813-3\/50012-6_rf0535","series-title":"Automation of Reasoning. Classical Papers on Computational Logic","first-page":"364","article-title":"A simplified proof method for elementary logic","author":"Kanger","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0530","series-title":"Automation of Reasoning. Classical Papers on Computational Logic","first-page":"364","article-title":"A simplified proof method for elementary logic","author":"Kanger","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0535","series-title":"Introduction to Metamathematics","author":"Kleene","year":"1952"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0540","series-title":"Computational Problems in Abstract Algebra","first-page":"263","article-title":"Simple word problems in universal algebras","author":"Knuth","year":"1970"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0545","series-title":"Canonical inference, Technical report, Department of Mathematics","author":"Lankford","year":"1975"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0550","series-title":"Symbolic Logic and Mechanical Theorem Proving","author":"Lee","year":"1973"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0555","first-page":"58","article-title":"A normal form of derivations in predicate calculus with equality and function symbols","volume":"4","author":"Lifschitz","year":"1967","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"key":"10.1016\/B978-044450813-3\/50012-6_rf0570","first-page":"5","article-title":"Specialized forms of derivation in predicate calculus with equality and functional symbols","volume":"Vol. 98","author":"Lifschitz","year":"1968","journal-title":"Trudy MIAN"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50012-6_bb0565","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00245018","article-title":"What is the inverse method?","volume":"5","author":"Lifschitz","year":"1989","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0570","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1090\/S0002-9947-1978-0469886-1","article-title":"The Diophantine problem for addition and divisibility","volume":"235","author":"Lipshitz","year":"1978","journal-title":"Transactions of the American Mathematical Society"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50012-6_bb0575","first-page":"41","article-title":"Some remarks on the Diophantine problem for addition and divisibility","volume":"33","author":"Lipshitz","year":"1981","journal-title":"Bull. Soc. Math. Belg. S\u00e9r. B"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0580","series-title":"Automated Theorem Proving: a Logical Basis","author":"Loveland","year":"1978"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0585","series-title":"Logic Programming and Automated Reasoning. International Conference LPAR'92.","first-page":"96","article-title":"Controlling redundancy in large search spaces: Argonne-style theorem proving through the years","author":"Lusk","year":"1992"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50012-6_bb0590","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1006\/jsco.1996.0075","article-title":"Oriented equational logic is complete","volume":"23","author":"Lynch","year":"1997","journal-title":"Journal of Symbolic Computations"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50012-6_bb0595","first-page":"147","article-title":"The problem of solvability of equations in free semigroups","volume":"103","author":"Makanin","year":"1977","journal-title":"Mat. Sbornik (in Russian)"},{"issue":"5","key":"10.1016\/B978-044450813-3\/50012-6_bb0600","first-page":"588","article-title":"Universal extended theories of integers","volume":"16","author":"Mart'janov","year":"1977","journal-title":"Algebra i Logika"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0605","first-page":"1420","article-title":"The inverse method of establishing deducibility in the classical predicate calculus","volume":"5","author":"Maslov","year":"1964","journal-title":"Soviet Mathematical Doklady"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0610","first-page":"80","article-title":"The generalization of the inverse method to predicate calculus with equality","volume":"20","author":"Maslov","year":"1971","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0615","series-title":"Automation of Reasoning (Classical papers on Computational Logic)","first-page":"48","article-title":"An inverse method for establishing deducibility of nonprenex formulas of the predicate calculus","author":"Maslov","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0620","series-title":"Automation of Reasoning (Classical papers on Computational Logic)","first-page":"264","article-title":"Relationship between tactics of the inverse method and the resolution method","author":"Maslov","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0625","series-title":"Theory of Deductive Systems and its Applications","author":"Maslov","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0630","series-title":"Mathematical Logic and Automatic Theorem Proving","first-page":"291","article-title":"The proof-search theory and the inverse method","author":"Maslov","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0635","series-title":"Automation of Reasoning (Classical papers on Computational Logic)","first-page":"29","article-title":"Mechanical proof-search and the theory of logical deduction in the USSR","author":"Maslov","year":"1983"},{"issue":"5","key":"10.1016\/B978-044450813-3\/50012-6_bb0640","first-page":"1029","article-title":"Two variants of classical predicate calculus without structure rule","volume":"147","author":"Matulis","year":"1962","journal-title":"Soviet Mathematical Doklady"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0645","first-page":"768","article-title":"On variants of classical predicate calculus with the unique deduction tree","volume":"148","author":"Matulis","year":"1963","journal-title":"Soviet Mathematical Doklady"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0650","series-title":"Computational Logic. Essays in Honor of Alan Robinson","first-page":"613","article-title":"Theory of disjunctive logic programs","author":"Minker","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0655","series-title":"COLOG-88","first-page":"198","article-title":"Gentzen-type systems and resolution rules. Part I. Propositional logic","author":"Mints","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0660","series-title":"\u201cProof Theory of Modal Logic\u201d, Studies in Pure and Applied Logic","article-title":"Transfer of sequent calculus strategies to resolution","author":"Mints","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0665","article-title":"Model elimination with basic ordered paramodulation","author":"Moser","year":"1995","journal-title":"Technical Report AR-95-11, Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen"},{"key":"10.1016\/B978-044450813-3\/50012-6_rf0680","article-title":"STE-modification revisited","author":"Moser","year":"1997","journal-title":"Technical Report AR-97-03, Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0675","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/0020-0190(93)90226-Y","article-title":"Simple LPO constraint solving methods","volume":"47","author":"Nieuwenhuis","year":"1993","journal-title":"Information Processing Letters"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0680","series-title":"ESOP'92","first-page":"371","article-title":"Basic superposition is complete","author":"Nieuwenhuis","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0685","series-title":"11th International Conference on Automated Deduction (CADE)","first-page":"477","article-title":"Theorem proving with ordering constrained clauses","author":"Nieuwenhuis","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0690","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1006\/jsco.1995.1020","article-title":"Theorem proving with ordering and equality constrained clauses","volume":"19","author":"Nieuwenhuis","year":"1995","journal-title":"Journal of Symbolic Computations"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0695","first-page":"335","article-title":"Computing small clause normal forms","volume":"Vol. I","author":"Nonnengart","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0700","series-title":"The Theory of Logical Inference","article-title":"On the size of derivations under minus-normalization in Russian","author":"Norgela","year":"1974"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0705","first-page":"152","article-title":"On nonlengthening applications of equality rules","volume":"16","author":"Orevkov","year":"1969","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0710","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0747-7171(08)80130-7","article-title":"Using forcing to prove completeness of resolution and paramodulation","volume":"11","author":"Pais","year":"1991","journal-title":"Journal of Symbolic Computations"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0715","series-title":"JELIA'94","first-page":"152","article-title":"A complete connection calculus with rigid E-unification","author":"Petermann","year":"1994"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50012-6_bb0720","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1137\/0212006","article-title":"A technique for establishing completeness results in theorem proving with equality","volume":"12","author":"Peterson","year":"1983","journal-title":"SIAM Journal of Computing"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0725","article-title":"Special cases and substitutes for rigid E-unification","author":"Plaisted","year":"1995","journal-title":"Technical Report MPI-I-95-2-010, Max-Planck-Institut f\u00fcr Informatik"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0730","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","article-title":"A structure-preserving clause form translation","volume":"2","author":"Plaisted","year":"1986","journal-title":"Journal of Symbolic Computations"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0735","first-page":"175","article-title":"Elimination of cut-type rules in axiomatic theories with equality","volume":"16","author":"Pliu\u0161kevi\u010diene","year":"1969","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"issue":"2","key":"10.1016\/B978-044450813-3\/50012-6_bb0740","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1111\/j.1755-2567.1960.tb00558.x","article-title":"An improved proof procedure","volume":"26","author":"Prawitz","year":"1960","journal-title":"Theoria"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0745","series-title":"Automation of Reasoning. Classical Papers on Computational Logic","first-page":"162","article-title":"An improved proof procedure","author":"Prawitz","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0750","series-title":"Machine Intelligence","first-page":"135","article-title":"Paramodulation and theorem-proving in first order theories with equality","author":"Robinson","year":"1969"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50012-6_bb0755","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0760","series-title":"Machine Intelligence","first-page":"77","article-title":"The generalized resolution principle","author":"Robinson","year":"1968"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0765","first-page":"175","article-title":"On sequential modifications of applied predicate calculi","volume":"4","author":"Rogava","year":"1967","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0770","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1016\/S0747-7171(08)80131-9","article-title":"Theorem proving with resolution and superposition: an extension of the Knuth and Bendix completion procedure as a complete set of inference rules","volume":"11","author":"Rusinowitch","year":"1991","journal-title":"Journal of Symbolic Computations"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50012-6_bb0775","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/BF00881952","article-title":"Tableau-based theorem provers: Systems and implementations","volume":"13","author":"Schumann","year":"1994","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50012-6_rf0790","series-title":"Beweistheorie","author":"Sch\u00fctte","year":"1960"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0785","series-title":"11th International Conference on Automated Deduction","first-page":"522","article-title":"Proof search in the intuitionistic sequent calculus","author":"Shankar","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0790","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1145\/359545.359570","article-title":"An algorithm for reasoning about equality","volume":"21","author":"Shostak","year":"1978","journal-title":"Communications of the ACM"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50012-6_bb0795","doi-asserted-by":"crossref","first-page":"622","DOI":"10.1145\/321850.321859","article-title":"Automated theorem-proving for theories with simplifiers, commutativity and associativity","volume":"21","author":"Slagle","year":"1974","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0800","series-title":"First-Order Logic","author":"Smullyan","year":"1968"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0805","series-title":"Rewriting Techniques and Applications","first-page":"150","article-title":"Goal-directed strategies for paramodulation","author":"Snyder","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0810","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF00244275","article-title":"Automated deduction by theory resolution","volume":"1","author":"Stickel","year":"1985","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0815","series-title":"Automated Deduction \u2014 CADE-13","first-page":"2","article-title":"A resolution theorem prover for intutionistic logic","author":"Tammet","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0820","article-title":"Uniform representation of recursively enumerable sets with simultaneous rigid E-unification","author":"Veanes","year":"1996","journal-title":"UPMAIL Technical Report 126, Uppsala University, Computing Science Department"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0825","article-title":"On Simultaneous Rigid E-Unification","author":"Veanes","year":"1997","journal-title":"PhD thesis, Uppsala University"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0830","series-title":"Computational Logic and Proof Theory. 5th Kurt G\u00f6del Colloquium, KGC'97","first-page":"305","article-title":"The undecidability of simultaneous rigid E-unification with two variables","author":"Veanes","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0835","article-title":"The relation between second-order unification and simultaneous rigid E-unification","author":"Veanes","year":"1998","journal-title":"Technical Report MPI-I-98-2-005, Max-Planck Institut f\u00fcr Informatik, Saarbr\u00fccken"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0840","series-title":"Proc. Thirteenth Annual IEEE Symposium on Logic in Computer Science","first-page":"264","article-title":"The relation between second-order unification and simultaneous rigid E-unification","author":"Veanes","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0845","article-title":"On Herbrand skeletons","author":"Voda","year":"1995","journal-title":"Technical report, Institute of Informatics, Comenius University Bratislava"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0850","first-page":"109","article-title":"A proof search method","volume":"107","author":"Voronkov","year":"1985","journal-title":"Vychislitelnye Sistemy"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0855","series-title":"Proc. 10th Int. Conf. on Automated Deduction","first-page":"677","article-title":"LISS \u2014 the logic inference search system","author":"Voronkov","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0860","series-title":"COLOG'88","first-page":"327","article-title":"A proof-search method for the first order logic","author":"Voronkov","year":"1990"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0865","series-title":"11th International Conference on Automated Deduction","first-page":"648","article-title":"Theorem proving in non-standard logics based on the inverse method","author":"Voronkov","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50012-6_rf0880","article-title":"On proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-Unification","author":"Voronkov","year":"1996","journal-title":"UPMAIL Technical Report 121, Uppsala University, Computing Science Department"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0875","series-title":"Theorem Proving with Analytic Tableaux and Related Methods. 5th International Workshop, TABLEAUX '96","first-page":"312","article-title":"Proof search in intuitionistic logic based on constraint satisfaction","author":"Voronkov","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0880","article-title":"Proof-search in intuitionistic logic based on the constraint satisfaction","author":"Voronkov","year":"1996","journal-title":"UPMAIL Technical Report 120, Uppsala University, Computing Science Department"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0885","series-title":"Automated Deduction \u2014 CADE-13","first-page":"32","article-title":"Proof search in intuitionistic logic with equality, or back to simultaneous rigid E-unification","author":"Voronkov","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0890","series-title":"Proc. IEEE Conference on Logic in Computer Science (LICS)","first-page":"252","article-title":"Herbrand's theorem, automated reasoning and semantic tableaux","author":"Voronkov","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0895","article-title":"Herbrand's theorem, automated reasoning and semantic tableaux","author":"Voronkov","year":"1998","journal-title":"UP-MAIL Technical Report 151, Uppsala University, Computing Science Department"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0900","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1023\/A:1005934721802","article-title":"Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification","volume":"21","author":"Voronkov","year":"1998","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0905","article-title":"Simultaneous rigid E-unification and other decision problems related to Herbrand's theorem","author":"Voronkov","year":"1998","journal-title":"UPMAIL Technical Report 152, Uppsala University, Computing Science Department"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0910","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1016\/S0304-3975(98)00317-X","article-title":"Simultaneous rigid E-unification and other decision problems related to Herbrand's theorem","volume":"224","author":"Voronkov","year":"1999","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0915","series-title":"Principles of Knowledge Representation and Reasoning (KR'2000)","first-page":"198","article-title":"Deciding K using K","author":"Voronkov","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0920","series-title":"Proc. 15th Annual IEEE Symp. on Logic in Computer Science","first-page":"401","article-title":"How to optimize proof-search in modal logics: a new way of proving redundancy criteria for sequent calculi","author":"Voronkov","year":"2000"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50012-6_bb0925","first-page":"1","article-title":"How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi","volume":"1","author":"Voronkov","year":"2001","journal-title":"ACM Transactions on Computational Logic"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0930","first-page":"1","article-title":"Proof-search in intuitionistic logic based on the constraint satisfaction and related complexity problems","author":"Voronkov","year":"2001","journal-title":"Logic Journal of the IGPL"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0935","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1147\/rd.41.0002","article-title":"Towards mechanical mathematics","volume":"4","author":"Wang","year":"1960","journal-title":"IBM J. of Research and Development"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0940","first-page":"1965","article-title":"Combining superposition, sorts and splitting","volume":"Vol. II","author":"Weidenbach","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0945","series-title":"Computational Logic. Essays in Honor of Alan Robinson","first-page":"3","article-title":"Subsumption, a sometimes undervalued procedure","author":"Wos","year":"1991"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0950","doi-asserted-by":"crossref","first-page":"698","DOI":"10.1145\/321420.321429","article-title":"The concept of demodulation in theorem proving","volume":"14","author":"Wos","year":"1967","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/B978-044450813-3\/50012-6_bb0955","series-title":"9th International Conference on Automated Deduction","first-page":"1","article-title":"First-order theorem proving using conditional rewrite rules","author":"Zhang","year":"1988"}],"container-title":["Handbook of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500126?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500126?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2023,5,12]],"date-time":"2023-05-12T10:27:08Z","timestamp":1683887228000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444508133500126"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9780444508133"],"references-count":192,"URL":"https:\/\/doi.org\/10.1016\/b978-044450813-3\/50012-6","relation":{},"subject":[],"published":{"date-parts":[[2001]]}}}