{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T14:09:06Z","timestamp":1726409346716},"publisher-location":"Cham","reference-count":84,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319418414"},{"type":"electronic","value":"9783319418421"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-41842-1_11","type":"book-chapter","created":{"date-parts":[[2017,2,1]],"date-time":"2017-02-01T17:01:15Z","timestamp":1485968475000},"page":"285-314","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["What Is Essential Unification?"],"prefix":"10.1007","author":[{"given":"Peter","family":"Szabo","sequence":"first","affiliation":[]},{"given":"J\u00f6rg","family":"Siekmann","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Hoche","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,1,31]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Adian, S. I., & Durnev, V. G. (2000). Decision problems for groups and semigroups. Russian Mathematical Surveys, 55(2), 207.","DOI":"10.1070\/RM2000v055n02ABEH000267"},{"issue":"3","key":"11_CR2","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/BF02328451","volume":"2","author":"F Baader","year":"1986","unstructured":"Baader, F. (1986). Unification in idempotent semigroups is of type zero. Journal of Automated Reasoning, 2(3), 283\u2013286.","journal-title":"Journal of Automated Reasoning"},{"key":"11_CR3","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/0020-0190(88)90098-1","volume":"27","author":"F Baader","year":"1988","unstructured":"Baader, F. (1988). A note on unification type zero. Information Processing Letters, 27, 91\u201393.","journal-title":"Information Processing Letters"},{"key":"11_CR4","unstructured":"Baader, F., Binh, N. Th., Borgwardt, S., & Morawska, B. (2015). Deciding unifiability and computing local unifiers in the description logic $$\\cal {EL} $$ EL without top constructor. Notre Dame Journal of Formal Logic."},{"key":"11_CR5","unstructured":"Baader, F., & Ghilardi, S. (2011). Unification in modal and description logics. Logic Journal of the IGPL, 19(6), 705\u2013730. http:\/\/jigpal.oxfordjournals.org\/content\/19\/6\/705.abstract ."},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Baader, F., & Nipkow, T. (1998). Term rewriting and all that. Cambridge University Press.","DOI":"10.1017\/CBO9781139172752"},{"key":"11_CR7","unstructured":"Baader, F., & Siekmann, J. (1994). General unification theory. In D.\u00a0Gabbay, C.\u00a0Hogger & J.\u00a0Robinson (Eds.), Handbook of logic in artificial intelligence and logic programming (pp. 41\u2013126). Oxford University Press."},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Baader, F., & Snyder, W. (2001). Unification theory. In A.\u00a0Robinson & A.\u00a0Voronkov (Eds.), Handbook of automated reasoning (Vol. 1). Elsevier Science Publishers.","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"11_CR9","unstructured":"Baader, F., Borgwardt, S., & Morawska, B. (2015). Dismatching and local disunification in $$\\cal {EL}$$ EL . In M. Fern\u00e1ndez (Ed.), Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA\u201915). Volume\u00a036 of Leibniz International Proceedings in Informatics, Warsaw, Poland. Dagstuhl Publishing."},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Baader, F., Gil, O. F., & Morawska, B. (2013). Hybrid unification in the description logic $$\\cal {EL}$$ EL . In B. Morawska & K. Korovin (Eds.), Proceedings of the 27th International Workshop on Unification (UNIF\u201913). The Netherlands: Eindhoven.","DOI":"10.25368\/2022.197"},{"key":"11_CR11","unstructured":"Baader, F., & Morawska, B. (2014). Matching with respect to general concept inclusions in the description logic $$\\cal {EL}$$ EL . In C. Lutz & M. Thielscher (Eds.), Proceedings of the 37th German Conference on Artificial Intelligence (KI\u201914). Volume 8736 of Lecture Notes in Artificial Intelligence (pp. 135\u2013146). Springer."},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Buerckert, H. J., Herold, A., Kapur, D., Siekmann, J., Stickel, M., Tepp, M., et al. (1988). Opening the AC-unification race. Journal of Automated Reasoning, 4(4), 465\u2013474.","DOI":"10.1007\/BF00297251"},{"key":"11_CR13","unstructured":"Bulitko, V. K. (1970). Equations and inequalities in a free group and semigroup. Geometr. i Algebra Tul. Gos. Ped. Inst. Ucen. Zap. Mat. Kafedr., 2, 242\u2013252."},{"key":"11_CR14","unstructured":"Charatonik, W., & Pacholski, L. (1993). Word equations with two variables. Word Equations and Related Topics, IWWERT (pp. 43\u201356). Berlin: Springer."},{"key":"11_CR15","unstructured":"Choffrut, Ch., & Karhumaeki, J. (1997). Combinatorics of words. In Handbook of formal languages (pp. 329\u2013438). Berlin: Springer."},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Dabrowski, R., & Plandowski, W. (2002, 2011). On word equations in one variable. Lecture Notes in Computer Science, 2420, 212\u2013220 and In Algorithmica, 60(4), 819\u2013828.","DOI":"10.1007\/s00453-009-9375-3"},{"key":"11_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-81952-0_1","volume-title":"Automation of reasoning 1: Classical papers on computational logic 1957\u20131966","author":"M Davis","year":"1983","unstructured":"Davis, M. (1983). The prehistory and early history of automated deduction. In J. Siekmann & G. Wrightson (Eds.), Automation of reasoning 1: Classical papers on computational logic 1957\u20131966 (pp. 1\u201328). Berlin: Springer."},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Davis, M. (1973). Hilbert\u2019s tenth problem is unsolvable. American Mathematical Monthly 233\u2013269.","DOI":"10.1080\/00029890.1973.11993265"},{"key":"11_CR19","unstructured":"Davis, M., & Hersh, R. (1984). Hilbert\u2019s 10th problem. Mathematics: People, Problems, Results, 2, 136\u2013148."},{"issue":"3","key":"11_CR20","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., & Putnam, H. (1960). A computing procedure for quantification theory. Journal of the ACM (JACM), 7(3), 201\u2013215.","journal-title":"Journal of the ACM (JACM)"},{"key":"11_CR21","doi-asserted-by":"publisher","first-page":"425","DOI":"10.2307\/1970289","volume":"74","author":"M Davis","year":"1961","unstructured":"Davis, M., Putnam, H., & Robinson, J. (1961). The decision problem for exponential diophantine equations. Annals of Mathematics, 74, 425\u2013436.","journal-title":"Annals of Mathematics"},{"key":"11_CR22","unstructured":"Dershowitz, N., & Jouannaud, J.-P. (1990). Rewrite systems. In J.\u00a0van Leeuwen (Ed.), Handbook of theoretical computer science (pp. 244\u2013320). North-Holland: Elsevier Science Publishers."},{"key":"11_CR23","first-page":"162","volume":"43","author":"N Dershowitz","year":"1991","unstructured":"Dershowitz, N., & Jouannaud, J.-P. (1991). Notations for rewriting. Bulletin of the EATCS, 43, 162\u2013174.","journal-title":"Bulletin of the EATCS"},{"key":"11_CR24","unstructured":"Diekert, V. (2002). Makanin\u2019s algorithm. In M. Lothaire (Ed.), Algebraic combinatorics on words (Chap.\u00a012, pp. 387\u2013442). Cambridge University Press."},{"issue":"1","key":"11_CR25","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BF00263448","volume":"8","author":"E Domenjoud","year":"1992","unstructured":"Domenjoud, E. (1992). A technical note on AC-unification: The number of minimal unifiers of the AC equation. Journal of Automated Reasoning, 8(1), 39\u201344.","journal-title":"Journal of Automated Reasoning"},{"key":"11_CR26","first-page":"1","volume":"11","author":"DJ Dougherty","year":"1994","unstructured":"Dougherty, D. J., & Johann, P. (1994). An improved general E-unification method. Journal of Symbolic Computation, 11, 1\u201319.","journal-title":"Journal of Symbolic Computation"},{"key":"11_CR27","unstructured":"Durnev, V. (1997). Studying algorithmic problems for free semi-groups and groups. In Logical foundations of computer science (pp. 88\u2013101). Berlin: Springer."},{"issue":"5","key":"11_CR28","doi-asserted-by":"publisher","first-page":"1024","DOI":"10.1007\/BF01149791","volume":"16","author":"VG Durnev","year":"1974","unstructured":"Durnev, V. G. (1974). On equations in free semigroups and groups. Mathematical Notes of the Academy of Sciences of the USSR, 16(5), 1024\u20131028.","journal-title":"Mathematical Notes of the Academy of Sciences of the USSR"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Erne, M. (2009). Closure. Journal of the American Mathematical Society. In F. Mynard & E. Pearl (Ed.), Beyond topology, contemporary mathematics (pp. 163\u2013283). American Mathematical Society.","DOI":"10.1090\/conm\/486\/09510"},{"issue":"1","key":"11_CR30","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/0304-3975(86)90175-1","volume":"43","author":"F Fages","year":"1986","unstructured":"Fages, F., & Huet, G. (1986). Complete sets of unifiers and matchers in equational theories. Theoretical Computer Science, 43(1), 189\u2013200.","journal-title":"Theoretical Computer Science"},{"key":"11_CR31","unstructured":"Gallier, J. H. (1991). Unification procedures in automated deduction methods based on matings: A survey. Technical Report CIS-436, University of Pensylvania, Department of Computer and Information Science."},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., & Korovin, K. (2003). New directions in instantiation-based theorem proving. In Proceedings. 18th Annual IEEE Symposium on Logic in Computer Science, 2003 (pp. 55\u201364). IEEE.","DOI":"10.1109\/LICS.2003.1210045"},{"issue":"1","key":"11_CR33","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1147\/rd.41.0028","volume":"4","author":"PC Gilmore","year":"1960","unstructured":"Gilmore, P. C. (1960). A proof method for quantification theory: Its justification and realization. IBM Journal of research and development, 4(1), 28\u201335.","journal-title":"IBM Journal of research and development"},{"key":"11_CR34","unstructured":"Hmelevskij, J. I. (1964). The solution of certain systems of word equations. Dokl. Akad. Nauk SSSR Soviet Math., 5, 724."},{"key":"11_CR35","first-page":"1611","volume":"7","author":"JI Hmelevskij","year":"1966","unstructured":"Hmelevskij, J. I. (1966). Word equations without coefficients. Soviet Math. Dokl., 7, 1611\u20131613.","journal-title":"Soviet Math. Dokl."},{"key":"11_CR36","unstructured":"Hmelevskij, J. I. (1967). Solution of word equations in three unknowns. Dokl. Akad. Nauk SSSR Soviet Math., 5, 177."},{"key":"11_CR37","unstructured":"Hoche, M., Siekmann, J., & Szabo, P. (2008). String unification is essentially infinitary. In M. Marin (Ed.), The 22nd International Workshop on Unification (UNIF\u201908) (pp. 82\u2013102). Hagenberg, Austria."},{"key":"11_CR38","unstructured":"Hoche, M., Siekmann, J., & Szabo, P. (2016). String unification is essentially infinitary. IFCoLog Journal of Logics and their Applications."},{"issue":"1","key":"11_CR39","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jal.2004.12.001","volume":"4","author":"M Hoche","year":"2006","unstructured":"Hoche, M., & Szabo, P. (2006). Essential unifiers. Journal of Applied Logic, 4(1), 1\u201325.","journal-title":"Journal of Applied Logic"},{"key":"11_CR40","unstructured":"Howie, J. M. (1976). An introduction to semigroup theory. Academic Press."},{"key":"11_CR41","doi-asserted-by":"crossref","unstructured":"Huet, G. (2002). Higher order unification 30 years later. In Theorem proving in higher order logics (Vol. 2410, pp. 3\u201312). Springer LNCS.","DOI":"10.1007\/3-540-45685-6_2"},{"issue":"1\u20133","key":"11_CR42","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s10817-006-9046-x","volume":"38","author":"S Jacobs","year":"2007","unstructured":"Jacobs, S., & Waldmann, U. (2007). Comparing instance generation methods for automated reasoning. Journal of Automated Reasoning, 38(1\u20133), 57\u201378.","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"11_CR43","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1145\/78935.78938","volume":"27","author":"J Jaffar","year":"1990","unstructured":"Jaffar, J. (1990). Minimal and complete word unification. JACM, 27(1), 47\u201385.","journal-title":"JACM"},{"key":"11_CR44","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-642-39212-2_30","volume":"7966","author":"A Jez","year":"2013","unstructured":"Jez, A. (2013). One-variable word equation in linear time. ICALP, Lecture Notes in Computer Science, 7966, 324\u2013335.","journal-title":"ICALP, Lecture Notes in Computer Science"},{"key":"11_CR45","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/S0049-237X(08)72020-2","volume":"35","author":"S Kanger","year":"1963","unstructured":"Kanger, S. (1963). A simplified proof method for elementary logic. Studies in Logic and the Foundations of Mathematics, 35, 87\u201394.","journal-title":"Studies in Logic and the Foundations of Mathematics"},{"issue":"2","key":"11_CR46","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/BF00245463","volume":"9","author":"D Kapur","year":"1992","unstructured":"Kapur, D., & Narendran, P. (1992). Complexity of unification problems with associative-commutative operators. Journal of Automated Reasoning, 9(2), 261\u2013288.","journal-title":"Journal of Automated Reasoning"},{"key":"11_CR47","doi-asserted-by":"crossref","unstructured":"Kapur, D., & Narendran, P. (1992). Double-exponential complexity of computing a complete set of AC-unifiers. In Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, LICS92.","DOI":"10.1109\/LICS.1992.185515"},{"key":"11_CR48","unstructured":"Kirchner, C., & Kirchner, H. (2006). Rewriting solving proving. http:\/\/www.loria.fr\/~ckirchne\/=rsp\/rsp.pdf ."},{"key":"11_CR49","unstructured":"Korovin, K. (2009). An invitation to instantion-based reasoning: From theory to practice. In Proceedings of CADE 22, Springer Lecture Notes on AI (Vol. 5663, pp. 163\u2013166). Springer."},{"issue":"1","key":"11_CR50","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1145\/62029.62030","volume":"21","author":"K Knight","year":"1989","unstructured":"Knight, K. (1989). Unification: A multidisciplinary survey. ACM Computing Surveys (CSUR), 21(1), 93\u2013124.","journal-title":"ACM Computing Surveys (CSUR)"},{"issue":"2","key":"11_CR51","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1142\/S0129054111008088","volume":"122","author":"M Laine","year":"2011","unstructured":"Laine, M., & Plandowski, W. (2011). Word equations with one unknown. International Journal of Foundations of Computer Science, 122(2), 345\u2013375.","journal-title":"International Journal of Foundations of Computer Science"},{"key":"11_CR52","doi-asserted-by":"crossref","unstructured":"Lee, S.-J., & Plaisted, D. A. (1992). Eliminating duplication with the hyper-linking strategy. Journal of Automated Reasoning, 9(1), 25\u201342.","DOI":"10.1007\/BF00247825"},{"key":"11_CR53","unstructured":"Lentin, A. (1972). Equations in free monoids. In M. Nivat (Ed.), Automata, languages and programming. North Holland."},{"key":"11_CR54","unstructured":"Lentin, A., & Schuetzenberger, M. P. (1967). A combinatorial problem in the theory of free monoids. In R. C. Bose & T. E. Dowling (Eds.), Combinatorial mathematics (pp. 112\u2013144). University of North Carolina Press."},{"key":"11_CR55","unstructured":"Livesey, M., & Siekmann, J. (1975). Termination and decidability results for string unification. Report Memo CSM-12, Computer Centre, Essex University, England."},{"key":"11_CR56","doi-asserted-by":"crossref","unstructured":"Lothaire, M. (1997). Combinatorics on words. Volume\u00a017 of Encyclopedia of Mathematics. Addison-Wesley. (Reprinted from Cambridge University Press, Cambridge Mathematical Library (1983)).","DOI":"10.1017\/CBO9780511566097"},{"key":"11_CR57","doi-asserted-by":"crossref","unstructured":"Lothaire, M. (2002). Algebraic combinatorics on words. Cambridge University Press.","DOI":"10.1017\/CBO9781107326019"},{"key":"11_CR58","unstructured":"Makanin, G. S. (1977). The problem of solvability of equations in a free semigroup. Original in Russian: Mathematicheskii Sbornik, 103(2), 147\u2013236 (Math. USSR Sbornik, 32, 129\u2013198)."},{"key":"11_CR59","unstructured":"Markov, A. A. (1954). Theory of algorithms. Trudy Mathematicheskogo Instituta Imeni VA Steklova, Izdat.Akad. Nauk SSSR, 17, 1038."},{"key":"11_CR60","unstructured":"Matijasevich, Ju. V. (1970). Enumerable sets are diophantine. Dokl. Akad. Nauk SSSR 191=Soviet Math. Dokl., 11, 354-358, 279\u2013282."},{"key":"11_CR61","first-page":"61","volume":"8","author":"Y Matiyasevich","year":"1970","unstructured":"Matiyasevich, Y. (1970). The connection between Hilbert\u2019s 10th problem and systems of equations between words and lengths. Seminars in Mathematics, 8, 61\u201367.","journal-title":"Seminars in Mathematics"},{"issue":"3","key":"11_CR62","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1145\/990308.990312","volume":"51","author":"W Plandowski","year":"2004","unstructured":"Plandowski, W. (2004). Satisfiability of word equations with constants is in Pspace. JACM, 51(3), 483\u2013496.","journal-title":"JACM"},{"key":"11_CR63","unstructured":"Plotkin, G. (1972). Building-in equational theories. In B.\u00a0Meltzer & D.\u00a0Michie (Eds.), Machine Intelligence (Vol.\u00a07, pp. 73\u201390). Edinburgh University Press."},{"key":"11_CR64","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1111\/j.1755-2567.1960.tb00558.x","volume":"26","author":"D Prawitz","year":"1960","unstructured":"Prawitz, D. (1960). An improved proof procedure. Theoria, 26, 102\u2013139.","journal-title":"Theoria"},{"issue":"2","key":"11_CR65","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/1089208.1089210","volume":"13","author":"P Raulefs","year":"1979","unstructured":"Raulefs, P., Siekmann, J., Szabo, P., & Unvericht, E. (1979). A short survey on the state of the art in matching and unification problems. ACM Sigsam Bulletin, 13(2), 14\u201320.","journal-title":"ACM Sigsam Bulletin"},{"key":"11_CR66","unstructured":"Raulefs, P., & Siekmann, J. H. (1978). Unification of idempotent functions. Technical report, Fachbereich Informatik, Universit\u00e4t Kaiserslautern."},{"issue":"1","key":"11_CR67","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J. A. (1965). A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1), 23\u201341.","journal-title":"Journal of the ACM"},{"key":"11_CR68","unstructured":"RTA list of open problems (2008). http:\/\/rtaloop.pps.jussieu.fr ."},{"issue":"3","key":"11_CR69","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/BF02328450","volume":"2","author":"M Schmidt-Schauss","year":"1986","unstructured":"Schmidt-Schauss, M. (1986). Unification under associativity and idempotence is of type nullary. Journal of Automated Reasoning, 2(3), 277\u2013281.","journal-title":"Journal of Automated Reasoning"},{"key":"11_CR70","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF00881904","volume":"11","author":"K Schulz","year":"1993","unstructured":"Schulz, K. (1993). Word unification and transformations of generalized equations. Journal of Automated Reasoning, 11, 149\u2013184.","journal-title":"Journal of Automated Reasoning"},{"key":"11_CR71","doi-asserted-by":"crossref","unstructured":"Schulz, K. U. (1992). Makanin\u2019s algorithm for word equations: Two improvements and a generalization. In Proceedings of the First International Workshop on Word Equations and Related Topics (IWWERT90) (Vol. 572, pp. 85\u2013150). Springer LNCS.","DOI":"10.1007\/3-540-55124-7_4"},{"key":"11_CR72","unstructured":"Siekmann, J. (1975). String unification. Report CSM-7, Computer Centre, University of Essex."},{"key":"11_CR73","unstructured":"Siekmann, J. (1976). Unification and matching problems. PhD thesis, Essex University, Computer Science."},{"key":"11_CR74","doi-asserted-by":"crossref","unstructured":"Siekmann, J. (1979). Unification of commutative terms. In Notes in Computer Science. Volume\u00a072 of Proceedings of the International Symposium on Symbolic and Algebraic Manipulation (pp. 531\u2013545). EUROSAM\u201979, Springer.","DOI":"10.1007\/3-540-09519-5_53"},{"key":"11_CR75","unstructured":"Siekmann, J. (1984). Universal unification. In Proceedings of the 7th International Conference on Automated Deduction (pp. 1\u201342). London: Springer."},{"issue":"3 & 4","key":"11_CR76","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1016\/S0747-7171(89)80012-4","volume":"7","author":"J Siekmann","year":"1989","unstructured":"Siekmann, J. (1989). Unification theory. Journal of Symbolic Computation, 7(3 & 4), 207\u2013274.","journal-title":"Journal of Symbolic Computation"},{"key":"11_CR77","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/BF02573590","volume":"25","author":"J Siekmann","year":"1982","unstructured":"Siekmann, J., & Szabo, P. (1982). A noetherian and confluent rewrite system for idempotent semigroups. Semigroup Forum, 25, 83\u2013100.","journal-title":"Semigroup Forum"},{"key":"11_CR78","unstructured":"Siekmann, J., & Wrightson, G. (1983). Automation of reasoning: Classical papers on computational logic (Vols. 1 & 2). Berlin: Springer."},{"key":"11_CR79","unstructured":"Szabo, P., & Unvericht, E. (1982). D-unification has infinitely many mgus. Technical report, University of Karlsruhe, Inst. f. Informatik I."},{"key":"11_CR80","unstructured":"Szabo, P. (1982). Unifikationstheorie erster Ordnung. PhD thesis, University Karlsruhe."},{"issue":"1","key":"11_CR81","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1016\/j.tcs.2004.06.016","volume":"323","author":"C Urban","year":"2004","unstructured":"Urban, C., Pitts, A. M., & Gabbay, M. J. (2004). Nominal unification. Theoretical Computer Science, 323(1), 473\u2013497.","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"11_CR82","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/BF02236612","volume":"2","author":"G Veenker","year":"1967","unstructured":"Veenker, G. (1967). Beweisalgorithmen f\u00fcr die pr\u00e4dikatenlogik. Computing, 2(3), 263\u2013283.","journal-title":"Computing"},{"issue":"1","key":"11_CR83","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1147\/rd.41.0002","volume":"4","author":"H Wang","year":"1960","unstructured":"Wang, H. (1960). Toward mechanical mathematics. IBM Journal of Research and Development, 4(1), 2\u201322.","journal-title":"IBM Journal of Research and Development"},{"key":"11_CR84","doi-asserted-by":"crossref","unstructured":"Wirth, C.-P., Siekmann, J., Benzm\u00fcller, C., & Autexier, S. (2009). Jacques herbrand: Life, logic, and automated deduction. In D.\u00a0Gabbay & J.\u00a0Woods (Eds.), Handbook of the History of Logic, Volume 5\u2014Logic from Russell to Church. Elsevier.","DOI":"10.1016\/S1874-5857(09)70009-3"}],"container-title":["Outstanding Contributions to Logic","Martin Davis on Computability, Computational Logic, and Mathematical Foundations"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41842-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,23]],"date-time":"2022-07-23T05:39:33Z","timestamp":1658554773000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41842-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319418414","9783319418421"],"references-count":84,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41842-1_11","relation":{},"ISSN":["2211-2758","2211-2766"],"issn-type":[{"type":"print","value":"2211-2758"},{"type":"electronic","value":"2211-2766"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"31 January 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}