{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T22:53:52Z","timestamp":1773096832095,"version":"3.50.1"},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"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":[[2003,9]]},"DOI":"10.1023\/a:1027357912519","type":"journal-article","created":{"date-parts":[[2003,11,9]],"date-time":"2003-11-09T22:46:39Z","timestamp":1068417999000},"page":"33-72","source":"Crossref","is-referenced-by-count":113,"title":["Theorem Proving Modulo"],"prefix":"10.1007","volume":"31","author":[{"given":"Gilles","family":"Dowek","sequence":"first","affiliation":[]},{"given":"Th\u00e9r\u00e8se","family":"Hardin","sequence":"additional","affiliation":[]},{"given":"Claude","family":"Kirchner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"5146544_CR1","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L. and L\u00e9vy, J.-J.: Explicit substitutions, J. Funct. Programming\n                           1(4) (1991), 375-416.","journal-title":"J. Funct. Programming"},{"key":"5146544_CR2","doi-asserted-by":"publisher","first-page":"414","DOI":"10.2307\/2269949","volume":"36","author":"P. B. Andrews","year":"1971","unstructured":"Andrews, P. B.: Resolution in type theory, J. Symbolic Logic\n                           36 (1971), 414-432.","journal-title":"J. Symbolic Logic"},{"key":"5146544_CR3","doi-asserted-by":"crossref","unstructured":"Baader, F. and Nipkow, T.: Term Rewriting and All That, Cambridge University Press, 1998.","DOI":"10.1017\/CBO9781139172752"},{"key":"5146544_CR4","volume-title":"Proof methods for equational theories","author":"L. Bachmair","year":"1987","unstructured":"Bachmair, L.: Proof methods for equational theories, Ph.D. thesis, University of Illinois, Urbana-Champaign, IL, 1987, Revised version, August 1988."},{"issue":"2","key":"5146544_CR5","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1006\/inco.1995.1131","volume":"121","author":"L. Bachmair","year":"1995","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C. and Snyder, W.: Basic paramodulation, Inform. and Comput.\n                           121(2) (1995), 172-192.","journal-title":"Inform. and Comput."},{"issue":"3","key":"5146544_CR6","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1023\/A:1015761529444","volume":"28","author":"H. Barendregt","year":"2002","unstructured":"Barendregt, H. and Barendsen, E.: Autartik computations in formal proofs, J. Automated Reasoning\n                           28(3) (2002), 321-336.","journal-title":"J. Automated Reasoning"},{"key":"5146544_CR7","series-title":"Lecture Notes in Comput. Sci.","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1007\/3-540-52885-7_87","volume-title":"Proceedings 10th International Conference on Automated Deduction, Kaiserslautern (Germany)","author":"H.-J. B\u00fcrckert","year":"1990","unstructured":"B\u00fcrckert, H.-J.: A resolution principle for clauses with constraints, in M. E. Stickel (ed.), Proceedings 10th International Conference on Automated Deduction, Kaiserslautern (Germany), Lecture Notes in Comput. Sci. 449, Springer-Verlag, New York, 1990, pp. 178-192."},{"key":"5146544_CR8","doi-asserted-by":"crossref","unstructured":"B\u00fcrckert, H.-J.: A Resolution Principle for a Logic with Restricted Quantifiers, Lecture Notes in Artificial Intelligence 568, Springer-Verlag, 1991.","DOI":"10.1007\/3-540-55034-8"},{"issue":"2","key":"5146544_CR9","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1145\/226643.226675","volume":"43","author":"P.-L. Curien","year":"1996","unstructured":"Curien, P.-L., Hardin, T. and L\u00e9vy, J.-J.: Confluence properties of weak and strong calculi of explicit substitutions, J. ACM\n                           43(2) (1996), 362-397.","journal-title":"J. ACM"},{"key":"5146544_CR10","doi-asserted-by":"crossref","unstructured":"Degtyarev, A. and Voronkov, A.: Equality reasoning in sequent-based calculi, in A. Robinson and A. Voronkov (eds.), Handbook of Automated Reasoning, Vol. I, Elsevier, 2001, Chapt. 10, pp. 611-706.","DOI":"10.1016\/B978-044450813-3\/50012-6"},{"key":"5146544_CR11","doi-asserted-by":"crossref","unstructured":"Dershowitz, N. and Jouannaud, J.-P.: Rewrite systems, in J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, Elsevier (North-Holland), 1990, Chapt. 6, pp. 244-320.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"5146544_CR12","doi-asserted-by":"crossref","unstructured":"Dowek, G.: Lambda-calculus, combinators and the comprehension scheme, in M. Dezan-Ciancaglini and G. Plotkin (eds.), Typed Lambda Calculi and Applications, Lecture Notes in Comput. Sci. 902, 1995, pp. 154-170.","DOI":"10.1007\/BFb0014051"},{"key":"5146544_CR13","doi-asserted-by":"crossref","unstructured":"Dowek, G.: Proof normalization for a first-order formulation of higher-order logic, in E. Gunter and A. Felty (eds.), Theorem Proving in Higher Order Logics, Lecture Notes in Comput. Sci. 1275, 1997, pp. 105-119.","DOI":"10.1007\/BFb0028389"},{"key":"5146544_CR14","unstructured":"Dowek, G.: La Part du Calcul, Universit\u00e9 de Paris 7, M\u00e9moire d'habilitation, 1999."},{"key":"5146544_CR15","doi-asserted-by":"crossref","unstructured":"Dowek, G.: Axioms vs. rewrite rules: From completeness to cut elimination, in H. Kirchner and C. Ringeissen (eds.), Frontiers of Combining Systems, Lecture Notes in Artificial Intelligence 1794, Springer-Verlag, 2000, pp. 62-72.","DOI":"10.1007\/10720084_5"},{"key":"5146544_CR16","unstructured":"Dowek, G., Hardin, T. and Kirchner, C.: Theorem proving modulo, Rapport de Recherche 3400, Institut National de Recherche en Informatique et en Automatique, 1998. http:\/\/www.inria.fr\/rrrt\/rr-3400.html."},{"key":"5146544_CR17","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1006\/inco.1999.2837","volume":"157","author":"G. Dowek","year":"2000","unstructured":"Dowek, G., Hardin, T. and Kirchner, C.: Higher-order unification via explicit substitutions, Inform. and Comput.\n                           157 (2000), 183-235.","journal-title":"Inform. and Comput."},{"issue":"1","key":"5146544_CR18","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1017\/S0960129500003236","volume":"11","author":"G. Dowek","year":"2001","unstructured":"Dowek, G., Hardin, T. and Kirchner, C.: HOL-?s, an intentional first-order expression of higher-order logic, Math. Structures Comput. Sci.\n                           11(1) (2001), 21-45.","journal-title":"Math. Structures Comput. Sci."},{"key":"5146544_CR19","unstructured":"Dowek, G., Hardin, T. and Kirchner, C.: Theorem proving modulo, revised version, Rapport de Recherche 4861, Institut National de Recherche en Informatique et en Automatique, 2003. http:\/\/www.inria.fr\/rrrt\/rr-4861.html."},{"key":"5146544_CR20","doi-asserted-by":"crossref","unstructured":"Dowek, G. and Werner, B.: Proof normalization modulo, in Types for Proofs and Programs, Lecture Notes in Comput. Sci. 1657, 1999, pp. 62-77.","DOI":"10.1007\/3-540-48167-2_5"},{"key":"5146544_CR21","series-title":"Computer Science and Technology Series","volume-title":"Logic for Computer Science: Foundations of Automatic Theorem Proving","author":"J. H. Gallier","year":"1986","unstructured":"Gallier, J. H.: Logic for Computer Science: Foundations of Automatic Theorem Proving, Computer Science and Technology Series 5, Harper & Row, New York, 1986."},{"key":"5146544_CR22","first-page":"151","volume-title":"Resolution of Equations in Algebraic Structures","author":"J. Gallier","year":"1989","unstructured":"Gallier, J., Raatz, S. and Snyder, W.: Rigid E-unification and its applications to equational matings, in H. A\u00eft-Kaci and M. Nivat (eds.), Resolution of Equations in Algebraic Structures, Vol. 1, Academic Press, New York, 1989, pp. 151-216."},{"key":"5146544_CR23","unstructured":"Girard, J.-Y., Lafont, Y. and Taylor, P.: Proofs and Types, Cambridge Tracts Theoret. Comput. Sci. 7, Cambridge University Press, 1989."},{"key":"5146544_CR24","unstructured":"Huet, G.: Constrained resolution: A complete method for type theory, Ph.D. thesis, Case Western Reserve University, 1972."},{"key":"5146544_CR25","unstructured":"Huet, G.: A mechanization of type theory, in Proceeding of the Third International Joint Conference on Artificial Intelligence, 1973, pp. 139-146."},{"issue":"1","key":"5146544_CR26","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"Huet, G.: A unification algorithm for typed lambda calculus, Theoret. Comput. Sci.\n                           1(1) (1975), 27-57.","journal-title":"Theoret. Comput. Sci."},{"key":"5146544_CR27","volume-title":"R\u00e9solution d'equations dans les langages d'ordre 1, 2,...,?","author":"G. Huet","year":"1976","unstructured":"Huet, G.: R\u00e9solution d'equations dans les langages d'ordre 1, 2,...,?, Th\u00e8se de Doctorat d'Etat, Universit\u00e9 de Paris 7, France, 1976."},{"key":"5146544_CR28","doi-asserted-by":"crossref","unstructured":"Hullot, J.-M.: Canonical forms and unification, in Proceedings 5th International Conference on Automated Deduction, Les Arcs (France), 1980, pp. 318-334.","DOI":"10.1007\/3-540-10009-1_25"},{"key":"5146544_CR29","doi-asserted-by":"crossref","unstructured":"Jaffar, J. and Lassez, J.-L.: Constraint logic programming, in Proceedings of the 14th Annual ACM Symposium on Principles Of Programming Languages, Munich (Germany), 1987, pp. 111-119.","DOI":"10.1145\/41625.41635"},{"issue":"4","key":"5146544_CR30","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J.-P. Jouannaud","year":"1986","unstructured":"Jouannaud, J.-P. and Kirchner, H.: Completion of a set of rules modulo a set of equations, SIAM J. Comput.\n                           15(4) (1986), 1155-1194. Preliminary version in Proceedings 11th ACM Symposium on Principles of Programming Languages, Salt Lake City (USA), 1984.","journal-title":"SIAM J. Comput."},{"key":"5146544_CR31","first-page":"257","volume-title":"Computational Logic. Essays in honor of Alan Robinson","author":"J.-P. Jouannaud","year":"1991","unstructured":"Jouannaud, J.-P. and Kirchner, C.: Solving equations in abstract algebras: A rule-based survey of unification, in J.-L. Lassez and G. Plotkin (eds.), Computational Logic. Essays in honor of Alan Robinson, MIT Press, Cambridge, MA, 1991, Chapt. 8, pp. 257-321."},{"key":"5146544_CR32","unstructured":"Kirchner, C.: M\u00e9thodes et outils de conception syst\u00e9matique d'algorithmes d'unification dans les th\u00e9ories \u00e9quationnelles, Th\u00e8se de Doctorat d'Etat, Universit\u00e9 Henri Poincar\u00e9 - Nancy 1, 1985."},{"key":"5146544_CR33","doi-asserted-by":"crossref","unstructured":"Kirchner, H.: Orderings in automated theorem proving, in F. Hoffman (ed.), Mathematical Aspects of Artificial Intelligence, Proc. Symposia Appl. Math. 55, Amer. Math. Soc., 1998, pp. 55-95.","DOI":"10.1090\/psapm\/055\/1619606"},{"issue":"3","key":"5146544_CR34","first-page":"9","volume":"4","author":"C. Kirchner","year":"1990","unstructured":"Kirchner, C., Kirchner, H. and Rusinowitch, M.: Deduction with symbolic constraints, Revue d'Intelligence Artificielle\n                           4(3) (1990), 9-52. Special issue on Automatic Deduction.","journal-title":"Revue d'Intelligence Artificielle"},{"key":"5146544_CR35","doi-asserted-by":"crossref","unstructured":"Kirchner, C. and Ringeissen, C.: Higher-order equational unification via explicit substitutions, in Proceedings 6th International Joint Conference ALP'97-HOA'97, Southampton (UK), Lecture Notes in Comput. Sci. 1298, Springer-Verlag, 1997, pp. 61-75.","DOI":"10.1007\/BFb0027003"},{"key":"5146544_CR36","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(93)90091-7","volume":"121","author":"J. Klop","year":"1993","unstructured":"Klop, J., van Oostrom, V. and van Raamsdonk, F.: Combinatory reduction systems: Introduction and survey, Theoret. Comput. Sci.\n                           121 (1993), 279-308.","journal-title":"Theoret. Comput. Sci."},{"key":"5146544_CR37","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D. E. Knuth","year":"1970","unstructured":"Knuth, D. E. and Bendix, P. B.: Simple word problems in universal algebras, in J. Leech (ed.), Computational Problems in Abstract Algebra, Pergamon Press, Oxford, 1970, pp. 263-297."},{"key":"5146544_CR38","unstructured":"Kolata, G.: With major math proof, brute computers show flash of reasoning power, New York Times, Tuesday, December 10, 1996."},{"issue":"2","key":"5146544_CR39","first-page":"217","volume":"1","author":"S.-J. Lee","year":"1994","unstructured":"Lee, S.-J. and Plaisted, D.: Use of replace rules in theorem proving, Methods of Logic in Computer Science\n                           1(2) (1994), 217-240.","journal-title":"Methods of Logic in Computer Science"},{"key":"5146544_CR40","doi-asserted-by":"crossref","unstructured":"March\u00e9, C.: Normalised rewriting and normalised completion, in S. Abramsky (ed.), Proceedings 9th IEEE Symposium on Logic in Computer Science, Paris, 1994, pp. 394-403.","DOI":"10.1109\/LICS.1994.316050"},{"issue":"3","key":"5146544_CR41","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"19","author":"W. McCune","year":"1997","unstructured":"McCune, W.: Solution of the Robbins problem, J. Automated Reasoning\n                           19(3) (1997), 263-276.","journal-title":"J. Automated Reasoning"},{"key":"5146544_CR42","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R. and Rubio, A.: AC-superposition with constraints: No AC-unifiers needed, in A. Bundy (ed.), Proceedings 12th International Conference on Automated Deduction, Nancy (France), Lecture Notes in Artificial Intelligence 814, Springer-Verlag, 1994, pp. 545-559.","DOI":"10.1007\/3-540-58156-1_40"},{"issue":"3-4","key":"5146544_CR43","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1016\/S0747-7171(89)80014-8","volume":"7","author":"W. Nutt","year":"1989","unstructured":"Nutt, W., R\u00e9ty, P. and Smolka, G.: Basic narrowing revisited, J. Symbolic Comput.\n                           7(3-4) (1989), 295-318. Special issue on unification. Part one.","journal-title":"J. Symbolic Comput."},{"issue":"1","key":"5146544_CR44","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1137\/0212006","volume":"12","author":"G. Peterson","year":"1983","unstructured":"Peterson, G.: A technique for establishing completeness results in theorem proving with equality, SIAM J. Comput.\n                           12(1) (1983), 82-100.","journal-title":"SIAM J. Comput."},{"key":"5146544_CR45","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. Peterson","year":"1981","unstructured":"Peterson, G. and Stickel, M. E.: Complete sets of reductions for some equational theories, J. ACM\n                           28 (1981), 233-264.","journal-title":"J. ACM"},{"issue":"1-2","key":"5146544_CR46","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0747-7171(08)80136-8","volume":"11","author":"D. A. Plaisted","year":"1991","unstructured":"Plaisted, D. A. and Potter, R. C.: Term rewriting: Some experimental results, J. Symbolic Comput.\n                           11(1-2) (1991), 149-180.","journal-title":"J. Symbolic Comput."},{"key":"5146544_CR47","first-page":"73","volume":"7","author":"G. Plotkin","year":"1972","unstructured":"Plotkin, G.: Building-in equational theories, Machine Intelligence\n                           7 (1972), 73-90.","journal-title":"Machine Intelligence"},{"issue":"4","key":"5146544_CR48","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/BF00244275","volume":"1","author":"M. Stickel","year":"1985","unstructured":"Stickel, M.: Automated deduction by theory resolution, J. Automated Reasoning\n                           1(4) (1985), 285-289.","journal-title":"J. Automated Reasoning"},{"key":"5146544_CR49","doi-asserted-by":"crossref","unstructured":"Stuber, J.: A model-based completeness proof of extended narrowing and resolution, in 1st Int. Joint Conf. on Automated Reasoning (IJCAR-2001), Siena, Italy, Lecture Notes in Comput. Sci. 2083, Springer-Verlag, 2001, pp. 195-210.","DOI":"10.1007\/3-540-45744-5_15"},{"key":"5146544_CR50","unstructured":"Terese (M. Bezem, J. W. Klop and R. de Vrijer, eds.): Term Rewriting Systems, Cambridge University Press, 2002."},{"key":"5146544_CR51","doi-asserted-by":"crossref","unstructured":"Vigneron, L.: Positive deduction modulo regular theories, in H. K. B\u00fcning (ed.), Annual Conference of the European Association for Computer Science Logic, Lecture Notes in Comput. Sci. 1092, Springer-Verlag, 1995, pp. 468-485. Selected papers.","DOI":"10.1007\/3-540-61377-3_54"},{"issue":"2","key":"5146544_CR52","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1016\/S0304-3975(01)00366-8","volume":"285","author":"P. Viry","year":"2002","unstructured":"Viry, P.: Equational rules for rewriting logic, Theoret. Comput. Sci.\n                           285(2) (2002), 487-517.","journal-title":"Theoret. Comput. Sci."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1027357912519.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1027357912519\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1027357912519.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:44:13Z","timestamp":1749123853000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1027357912519"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":52,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["5146544"],"URL":"https:\/\/doi.org\/10.1023\/a:1027357912519","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}