{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T13:50:13Z","timestamp":1648821013820},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1996,9,1]],"date-time":"1996-09-01T00:00:00Z","timestamp":841536000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[1996,9]]},"DOI":"10.1007\/bf02127750","type":"journal-article","created":{"date-parts":[[2005,9,15]],"date-time":"2005-09-15T11:34:26Z","timestamp":1126784066000},"page":"261-293","source":"Crossref","is-referenced-by-count":9,"title":["Unification in sort theories and its applications"],"prefix":"10.1007","volume":"18","author":[{"given":"Christoph","family":"Weidenbach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"BF02127750_CR1","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/0004-3702(92)90055-3","volume":"55","author":"C. Beierle","year":"1992","unstructured":"C. Beierle, U. Hedst\u00fcck, U. Pletat and J. Siekmann, An order-sorted logic for knowledge representation systems,Artificial Intelligence 55 (1992) 149\u2013191.","journal-title":"Artificial Intelligence"},{"key":"BF02127750_CR2","doi-asserted-by":"crossref","unstructured":"K.H. Bl\u00e4sius, U. Hedtst\u00fcck and C.-R. Rollinger (eds.),Sorts and Types in Artificial Intelligence, Workshop Proceedings, LNAI, Vol. 418 (Springer, 1990).","DOI":"10.1007\/3-540-52337-6"},{"key":"BF02127750_CR3","first-page":"161","volume":"577","author":"B. Bogaert","year":"1992","unstructured":"B. Bogaert and S. Tison, Equality and disequality constraints on direct subterms in tree automata, in:Proc. of 9th Annual Symposium on Theoretical Aspects of Computer Science, STACS92, LNCS, Vol. 577, eds. A. Finkel and M. Jantzen (Springer, 1992) pp. 161\u2013171.","journal-title":"Proc. of 9th Annual Symposium on Theoretical Aspects of Computer Science, STACS92"},{"key":"BF02127750_CR4","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1007\/3-540-58201-0_88","volume":"820","author":"A.-C. Caron","year":"1994","unstructured":"A.-C. Caron, H. Comon, J.-L. Coquid\u00e9, M. Dauchet and F. Jacquemard, Pumping, cleaning and symbolic constraints solving, in:Automata Languages and Programming, 21st International Colloquium, ICALP'94, LNCS, Vol. 820, eds. S. Abiteboul and E. Shamir (Springer, 1994) pp. 436\u2013447.","journal-title":"Automata Languages and Programming, 21st International Colloquium, ICALP'94"},{"issue":"2","key":"BF02127750_CR5","first-page":"113","volume":"3","author":"A.G. Cohn","year":"1987","unstructured":"A.G. Cohn, A more expressive formulation of many sorted logic,Journal of Automated Reasoning 3(2) (1987) 113\u2013200.","journal-title":"Journal of Automated Reasoning"},{"key":"BF02127750_CR6","first-page":"633","volume":"607","author":"A.G. Cohn","year":"1992","unstructured":"A.G. Cohn, A many sorted logic with possibly empty sorts, in:11th International Conference on Automated Deduction, CADE-11, LNCS, Vol. 607 (Springer, 1992) pp. 633\u2013647.","journal-title":"11th International Conference on Automated Deduction, CADE-11"},{"key":"BF02127750_CR7","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1007\/3-540-51081-8_101","volume":"355","author":"H. Comon","year":"1989","unstructured":"H. Comon, Inductive proofs by specification transformations, in:Rewriting Techniques and Applications, RTA-89, LNCS, Vol. 355 (Springer, 1989) pp. 76\u201391.","journal-title":"Rewriting Techniques and Applications, RTA-89"},{"key":"BF02127750_CR8","doi-asserted-by":"crossref","unstructured":"H. Comon, Equational formulas in order-sorted algebras, in:Proc. of ICALP (Springer, 1990) pp. 674\u2013688.","DOI":"10.1007\/BFb0032066"},{"key":"BF02127750_CR9","unstructured":"J. Corbin and M. Bidoit, A rehabilitation of Robinson's unification algorithm, in:Proceedings of IFIP 9th World Computer Congress (North-Holland, 1983) pp. 909\u2013914."},{"issue":"1","key":"BF02127750_CR10","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"N. Dershowitz, Termination of rewriting,Journal of Symbolic Computation 3(1) (1987) 69\u2013115.","journal-title":"Journal of Symbolic Computation"},{"key":"BF02127750_CR11","first-page":"243","volume":"B","author":"N. Dershowitz","year":"1990","unstructured":"N. Dershowitz and J.-P. Jouannaud, Rewrite systems, in:Handbook of Theoretical Computer Science, Vol. B, Chapter 6, ed. J. van Leeuwen (Elsevier Science Publishers, 1990) pp. 243\u2013320.","journal-title":"Handbook of Theoretical Computer Science"},{"issue":"3","key":"BF02127750_CR12","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"1","author":"W.F. Dowling","year":"1984","unstructured":"W.F. Dowling and J.H. Gallier, Linear-time algorithms for testing the satisfiability of propositional Horn formulae,Journal of Logic Programming 1(3) (1984) 267\u2013284.","journal-title":"Journal of Logic Programming"},{"key":"BF02127750_CR13","doi-asserted-by":"crossref","unstructured":"M. Fitting,First-Order Logic, Texts and Monographs in Computer Science (Springer, 1990).","DOI":"10.1007\/978-1-4684-0357-2_5"},{"key":"BF02127750_CR14","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1016\/0004-3702(91)90009-9","volume":"49","author":"A.M. Frisch","year":"1991","unstructured":"A.M. Frisch, The substitutional framework for sorted deduction: fundamental results on hybrid reasoning,Artificial Intelligence 49 (1991) 161\u2013198.","journal-title":"Artificial Intelligence"},{"key":"BF02127750_CR15","first-page":"178","volume":"607","author":"A.M. Frisch","year":"1992","unstructured":"A.M. Frisch and A.G. Cohn, An abstract view of sorted unification, in:11th International Conference on Automated Deduction, CADE-11, LNCS, Vol. 607 (Springer, 1992) pp. 178\u2013192.","journal-title":"11th International Conference on Automated Deduction, CADE-11"},{"key":"BF02127750_CR16","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0304-3975(92)90302-V","volume":"105","author":"J.A. Goguen","year":"1992","unstructured":"J.A. Goguen and J. Meseguer, Order-sorted algebra, I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations,Theoretical Computer Science 105 (1992) 217\u2013273.","journal-title":"Theoretical Computer Science"},{"key":"BF02127750_CR17","doi-asserted-by":"crossref","unstructured":"N. Guarino, M. Carrara and P. Giaretta, On ontology of meta-level categories, in:KR-94, Proceedings of the Fourth International Conference, eds. J. Doyle, E. Sandewall and P. Torasso (Morgan-Kaufmann, 1994) pp. 270\u2013280.","DOI":"10.1016\/B978-1-4832-1452-8.50121-4"},{"key":"BF02127750_CR18","unstructured":"J.-P. Jouannaud and C. Kirchner, Solving equations in abstract algebras: A rule-based survey of unification, in:Computational Logic, Essays in Honor of Alan Robinson, Chapter 8, eds. J.L. Lassez and G. Plotkin (MIT Press, 1991) pp. 257\u2013321."},{"key":"BF02127750_CR19","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/3-540-58156-1_26","volume":"814","author":"M. Kerber","year":"1994","unstructured":"M. Kerber and M. Kohlhase, A mechanization of strong kleene logic for partial functions, in:12th International Conference on Automated Deduction, CADE-12, LNAI, Vol. 814 (Springer, 1994) pp. 371\u2013385.","journal-title":"12th International Conference on Automated Deduction, CADE-12"},{"issue":"2","key":"BF02127750_CR20","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"A. Martelli and U. Montanari, An efficient unification algorithm,ACM Trans. Programming Languages ans Systems 4(2) (1982) 258\u2013282.","journal-title":"ACM Trans. Programming Languages ans Systems"},{"key":"BF02127750_CR21","unstructured":"J. Meseguer, J.A. Goguen and G. Smolka, Order-sorted unification, in:Unification, ed. C. Kirchner (Academic Press, 1990) pp. 457\u2013487."},{"key":"BF02127750_CR22","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/BF01396685","volume":"145","author":"A. Oberschelp","year":"1962","unstructured":"A. Oberschelp, Untersuchungen zur mehrsortigen Quantorenlogik,Mathematische Annalen 145 (1962) 297\u2013333.","journal-title":"Mathematische Annalen"},{"issue":"3","key":"BF02127750_CR23","first-page":"327","volume":"1","author":"H.-J. Ohlbach","year":"1985","unstructured":"H.-J. Ohlbach and M. Schmidt-Schau\u00df, The lion and the unicorn,Journal of Automated Reasoning 1(3) (1985) 327\u2013332.","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"BF02127750_CR24","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","volume":"16","author":"M. Paterson","year":"1978","unstructured":"M. Paterson and M. Wegman, Linear unification,Journal of Computer and System Sciences 16(2) (1978) 158\u2013167.","journal-title":"Journal of Computer and System Sciences"},{"key":"BF02127750_CR25","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1090\/S0002-9904-1946-08555-9","volume":"52","author":"E.L. Post","year":"1946","unstructured":"E.L. Post, A variant of a recursively unsolvable problem,Bulletin of the American Mathematical Society 52 (1946) 264\u2013268.","journal-title":"Bulletin of the American Mathematical Society"},{"key":"BF02127750_CR26","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1111\/j.1755-2567.1960.tb00558.x","volume":"26","author":"D. Prawitz","year":"1960","unstructured":"D. Prawitz, An improved proof procedure,Theoria 26 (1960) 102\u2013139.","journal-title":"Theoria"},{"issue":"1","key":"BF02127750_CR27","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"J.A. Robinson, A machine-oriented logic based on the resolution principle,Journal of the ACM 12(1) (1965) 23\u201341.","journal-title":"Journal of the ACM"},{"key":"BF02127750_CR28","unstructured":"G. Rozenberg and A. Salomaa,Cornerstones of Undecidability (Prentice-Hall, 1994)."},{"key":"BF02127750_CR29","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1007\/BF01448954","volume":"115","author":"A. Schmidt","year":"1938","unstructured":"A. Schmidt, \u00dcber deduktive Theorien mit mehreren Sorten von Grunddingen,Mathematische Annalen 115 (1938) 485\u2013506.","journal-title":"Mathematische Annalen"},{"key":"BF02127750_CR30","doi-asserted-by":"crossref","unstructured":"M. Schmidt-Schau\u00df,Computational Aspects of an Order Sorted Logic with Term Declarations, LNAI, Vol. 395 (Springer, 1989).","DOI":"10.1007\/BFb0024065"},{"key":"BF02127750_CR31","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/3-540-52337-6_18","volume":"418","author":"P.H. Schmitt","year":"1989","unstructured":"P.H. Schmitt and W. Wernecke, Tableau calculus for order sorted logic, in:Sorts and Types in Artificial Intelligence, LNAI, Vol. 418, eds. K.H. Bl\u00e4sius, U. Hedtst\u00fcck and C.-R. Rollinger (Springer, April 1989) pp. 49\u201360.","journal-title":"Sorts and Types in Artificial Intelligence"},{"key":"BF02127750_CR32","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/S0747-7171(89)80012-4","volume":"7","author":"J. Siekmann","year":"1989","unstructured":"J. Siekmann, Unification theory,Journal of Symbolic Computation, Special Issue on Unification 7 (1989) 207\u2013274.","journal-title":"Journal of Symbolic Computation, Special Issue on Unification"},{"key":"BF02127750_CR33","doi-asserted-by":"crossref","unstructured":"G. Smolka, Logic programming over polymorphically order-sorted types, PhD Thesis, Universit\u00e4t Kaiserslautern (May 1989).","DOI":"10.1007\/3-540-50667-5_58"},{"key":"BF02127750_CR34","first-page":"163","volume":"607","author":"T.E. Uribe","year":"1992","unstructured":"T.E. Uribe, Sorted unification using set constraints, in:11th International Conference on Automated Deduction, CADE-11, LNCS, Vol. 607 (Springer, 1992) pp. 163\u2013177.","journal-title":"11th International Conference on Automated Deduction, CADE-11"},{"key":"BF02127750_CR35","doi-asserted-by":"crossref","unstructured":"U. Waldmann, Semantics of order-sorted specifications,Journal of Theoretical Computer Science (1992) 1\u201335.","DOI":"10.1016\/0304-3975(92)90322-7"},{"key":"BF02127750_CR36","unstructured":"C. Walther, A mechanical solution of Schubert's steamroller by many-sorted resolution, in:Proceedings of the 4th AAAI (1984) pp. 330\u2013334. Revised version inArtificial Intelligence (26)2 (1985) 217\u2013224."},{"key":"BF02127750_CR37","doi-asserted-by":"crossref","unstructured":"C. Walther,A Many-sorted Calculus based on Resolution and Paramodulation, Research Notes in Artificial Intelligence (Pitman, 1987).","DOI":"10.1016\/B978-0-273-08718-2.50007-9"},{"key":"BF02127750_CR38","unstructured":"C. Weidenbach, A sorted logic using dynamic sorts, MPI-Report MPI-I-91-218, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken (December 1991)."},{"key":"BF02127750_CR39","unstructured":"C. Weidenbach, Extending the resolution method with sorts, in:Proc. of 13th International Joint Conference on Artificial Intelligence, IJCAI-93 (Morgan-Kaufmann, 1993) pp. 60\u201365."},{"key":"BF02127750_CR40","unstructured":"C. Weidenbach, Minimal resolution, MPI-Report MPI-I-94-227, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken (1994)."},{"issue":"6","key":"BF02127750_CR41","first-page":"887","volume":"3","author":"C. Weidenbach","year":"1995","unstructured":"C. Weidenbach, First-order tableaux with sorts,Journal of the Interest Group in Pure and Applied Logics, IGPL 3(6) (1995) 887\u2013906.","journal-title":"Journal of the Interest Group in Pure and Applied Logics, IGPL"},{"key":"BF02127750_CR42","unstructured":"L. Wos, R. Overbeek, E. Lusk and J. Boyle,Automated Reasoning, Introduction and Applications, 2nd edn. (McGraw-Hill, 1992)."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02127750.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF02127750\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02127750","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,9]],"date-time":"2020-04-09T14:02:30Z","timestamp":1586440950000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF02127750"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,9]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1996,9]]}},"alternative-id":["BF02127750"],"URL":"https:\/\/doi.org\/10.1007\/bf02127750","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,9]]}}}