{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:04Z","timestamp":1749124084935},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540167808"},{"type":"electronic","value":"9783540398615"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1986]]},"DOI":"10.1007\/3-540-16780-3_118","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T19:00:10Z","timestamp":1330196410000},"page":"538-552","source":"Crossref","is-referenced-by-count":13,"title":["Unification in many-sorted equational theories"],"prefix":"10.1007","author":[{"given":"Manfred","family":"Schmidt-Schauss","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"44_CR1","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/BF00246024","volume":"2","author":"W. Buettner","year":"1986","unstructured":"Buettner, W., \"Unification in the datastructure multiset\", Journal of Automated Reasoning, vol.2, pp. 75\u201388, (1986).","journal-title":"Journal of Automated Reasoning"},{"key":"44_CR2","unstructured":"Buettner,W., \"Unification in the datastructure set\", (to appear in this Proc. of 8th CADE)"},{"key":"44_CR3","volume-title":"Rewrite Systems on a Lattice of Types","author":"R.J. Cunningham","year":"1983","unstructured":"Cunningham, R.J., Dick, A.J.J., \"Rewrite Systems on a Lattice of Types\", Rep. No. DOC 83\/7, Imperial College, London SW7 (1983)"},{"key":"44_CR4","unstructured":"Cohn, A.G. \"Improving the Expressiveness of Many-sorted Logic.\", AAAI-83, Washington (1983)"},{"key":"44_CR5","unstructured":"Fages, F. \"Formes canonique dans les alg\u00e8bres boole\u00e8nnes et application \u00e0 la d\u00e8monstration automatique en logique de premier ordre.\" Th\u00e8se du 3eme cycle, Paris, (1983)"},{"key":"44_CR6","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J., \"Equality, Types, Modules and Generics for Logic Programming\", Journal of Logic Programming, (1984)","DOI":"10.1016\/0743-1066(84)90004-9"},{"key":"44_CR7","unstructured":"Goguen, J.A., Meseguer, J., \"Order Sorted Algebra I. Partial and Overloaded Operators, Errors and Inheritance.\", SRI Report (1985)"},{"key":"44_CR8","doi-asserted-by":"crossref","unstructured":"Gr\u00e4tzer, G., \"Universal algebra\", Springer Verlag, (1979)","DOI":"10.1007\/978-0-387-77487-9"},{"key":"44_CR9","unstructured":"Hayes, P., \"A Logic of Actions.\", Machine Intelligence 6, Metamathematics Unit, University of Edinburgh (1971)"},{"key":"44_CR10","unstructured":"Herold, A., \"Some basic notions of first order unification theory.\", Internal report 15\/83, Univ. Karlsruhe, (1983)"},{"key":"44_CR11","unstructured":"Herold, A.,Siekmann, J., \"Unification in abelian semigroups\", technical report, Universit\u00e4t Kaiserslautern, Memo SEKI-85-III, (1985)"},{"key":"44_CR12","doi-asserted-by":"crossref","unstructured":"Henschen, L.J., \"N-Sorted Logic for Automated Theorem Proving in Higher-Order Logic.\", Proc. ACM Conference Boston, (1972)","DOI":"10.1145\/800193.805823"},{"key":"44_CR13","unstructured":"Huet, G., \"Resolution d'equations dans des languages d'ordere 1,2,..., \u03c9;\";, These d'Etat, Univ. de Paris, VII, (1976)"},{"key":"44_CR14","doi-asserted-by":"crossref","unstructured":"Huet, G., Oppen, D.C., \"Equations and Rewrite Rules\", SRI Technical Report CSL-111, (1980)","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"44_CR15","first-page":"318","volume":"87","author":"J.M. Hullot","year":"1980","unstructured":"Hullot, J.M., \"Canonical forms and unification,\" Proc of the 5 th workshop on automated deduction, Springer Lecture Notes, vol. 87, pp. 318\u2013334, (1980)","journal-title":"Springer Lecture Notes"},{"key":"44_CR16","unstructured":"Karl Mark G. Raph, \"The Markgraf Karl Refutation Procedure\", Technical report, Univ. Kaiserslautern, Memo SEKI-84-03, (1984)"},{"key":"44_CR17","unstructured":"Loveland, D., \"Automated Theorem Proving\", North Holland, (1980)"},{"key":"44_CR18","unstructured":"Livesey,M., Siekmann, J., \"Unification of sets and multisets,\" Technical report, Unive Kaiserslautern, Memo-SEKI-76-01, (1976)"},{"key":"44_CR19","doi-asserted-by":"crossref","unstructured":"Oberschelp, A., \"Untersuchungen zur mehrsortigen Quantorenlogik.\", Mathematische Annalen 145 (1962)","DOI":"10.1007\/BF01396685"},{"key":"44_CR20","unstructured":"Plotkin, G., \"Building in equational theories.\", Machine Intelligence, vol. 7, 1972"},{"key":"44_CR21","doi-asserted-by":"crossref","unstructured":"Robinson, J.A., \"A Machine-Oriented Logic Based on the Resolution Principle.\" JACM 12 (1965)","DOI":"10.1145\/321250.321253"},{"key":"44_CR22","unstructured":"Schmidt-Schauss, M., \"A many-sorted calculus with polymorphic functions based on resolution and paramodulation.\", Proc 9 th IJCAI, Los Angeles,(1985)"},{"key":"44_CR23","doi-asserted-by":"crossref","unstructured":"Schmidt-Schauss, M., \"Unification in a many-sorted calculus with declarations.\", Proc. of GWAI, (1985)","DOI":"10.1007\/978-3-642-71145-9_9"},{"key":"44_CR24","unstructured":"Schmidt-Schauss, M., \"Unification in many-sorted equational theories.\", Internal report. Institut f\u00fcr Informatik, Kaiserslautern (forthcoming)"},{"key":"44_CR25","doi-asserted-by":"crossref","unstructured":"Siekmann, J. H., \"Universal Unification\", Proc. of the 7 th CADE, Napa California, (1984)","DOI":"10.1007\/978-0-387-34768-4_1"},{"key":"44_CR26","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1145\/322261.322262","volume":"28","author":"M.E. Stickel","year":"1981","unstructured":"Stickel, M.E., \"A unification algorithm for Associative-Commutative Functions\", JACM 28, pp. 423\u2013434, (1981)","journal-title":"JACM"},{"key":"44_CR27","unstructured":"Szabo, P., \"Theory of First order Unification.\", (in German, thesis) Univ. Karlsruhe, 1982"},{"key":"44_CR28","unstructured":"Walther, C., \"A Many-Sorted Calculus Based on Resolution and Paramodulation.\", Proc. of the 8 th I JCAI, Karlsruhe, (1983)"},{"key":"44_CR29","unstructured":"Walther, C., \"Unification in Many-Sorted Theories.\", Proc. of the 6 th ECAI, PISA, (1984)"}],"container-title":["Lecture Notes in Computer Science","8th International Conference on Automated Deduction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-16780-3_118.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T17:45:21Z","timestamp":1687283121000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-16780-3_118"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986]]},"ISBN":["9783540167808","9783540398615"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-16780-3_118","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1986]]}}}