{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:48:05Z","timestamp":1762458485088},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540643012"},{"type":"electronic","value":"9783540697213"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0052364","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T05:31:11Z","timestamp":1149658271000},"page":"106-120","source":"Crossref","is-referenced-by-count":4,"title":["E-unification for subsystems of S4"],"prefix":"10.1007","author":[{"given":"Renate A.","family":"Schmidt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,18]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Arnborg, S. and Tid\u00e9n, E. (1985), Unification problems with one-sided distributivity, in J.-P. Jouannaud (ed.), Proc. Intern. Conf. on Rewriting Techniques and Applications, Vol. 202 of LNCS, Springer, pp. 398\u2013406.","DOI":"10.1007\/3-540-15976-2_20"},{"issue":"3","key":"9_CR2","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1093\/logcom\/2.3.247","volume":"2","author":"Y. Auffray","year":"1992","unstructured":"Auffray, Y. and Enjalbert, P. (1992), Modal theorem proving: An equational viewpoint, Journal of Logic and Computation 2(3), 247\u2013297.","journal-title":"Journal of Logic and Computation"},{"issue":"1","key":"9_CR3","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1006\/inco.1994.1043","volume":"111","author":"H. Comon","year":"1994","unstructured":"Comon, H., Haberstrau, M. and Jouannaud, J.-P. (1994), Syntacticness, cyclesyntacticness and shallow theories, Information and Computation 111(1), 154\u2013191.","journal-title":"Information and Computation"},{"key":"9_CR4","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0304-3975(91)90182-2","volume":"85","author":"N. Doggaz","year":"1991","unstructured":"Doggaz, N. and Kirchner, C. (1991), Completion for unification, Theoretical Computer Science 85, 231\u2013251.","journal-title":"Theoretical Computer Science"},{"key":"9_CR5","unstructured":"Farinas del Cerro, L. and Herzig, A. (1989), Automated quantified modal logic, in P. B. Brazdil and K. Konolige (eds), Machine Learning, Meta-Reasoning and Logics, Kluwer, pp. 301\u2013317."},{"key":"9_CR6","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1093\/oso\/9780198537915.003.0008","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 4","author":"L. Farinas del Cerro","year":"1995","unstructured":"Farinas del Cerro, L. and Herzig, A. (1995), Modal deduction with applications in epistemic and temporal logics, in D. M. Gabbay, C. J. Hogger and J. A. Robinson (eds), Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 4, Clarendon Press, Oxford, pp. 499\u2013594."},{"key":"9_CR7","volume-title":"PhD thesis","author":"A. Herzig","year":"1989","unstructured":"Herzig, A. (1989), Raisonnement automatique en logique modale et algorithmes d'unification., PhD thesis, Univ. Paul-Sabatier, Toulouse."},{"issue":"1","key":"9_CR8","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1145\/78935.78938","volume":"37","author":"J. Jaffar","year":"1990","unstructured":"Jaffar, J. (1990), Minimal and complete word unification, J. ACM 37(1), 47\u201385.","journal-title":"J. ACM"},{"key":"9_CR9","unstructured":"Jouannaud, J.-P. and Kirchner, C. (1991), 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, pp. 257\u2013321."},{"key":"9_CR10","first-page":"270","volume-title":"Syntactic theories and unification","author":"C. Kirchner","year":"1990","unstructured":"Kirchner, C. and Klay, F. (1990), Syntactic theories and unification, in J. C. Mitchell (ed.), Proc. LICS'90, IEEE Computer Society Press, Philadelphia, pp. 270\u2013277."},{"issue":"2","key":"9_CR11","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1070\/SM1977v032n02ABEH002376","volume":"32","author":"G. S. Makanin","year":"1977","unstructured":"Makanin, G. S. (1977), The problem of solvability of equations in a free semigroup, Math. USSR Sbornik 32(2), 129\u2013198.","journal-title":"Math. USSR Sbornik"},{"key":"9_CR12","volume-title":"PhD thesis","author":"H. J. Ohlbach","year":"1988","unstructured":"Ohlbach, H. J. (1988), A Resolution Calculus for Modal Logics, PhD thesis, Univ. Kaiserslautern, Germany."},{"issue":"5","key":"9_CR13","doi-asserted-by":"publisher","first-page":"691","DOI":"10.1093\/logcom\/1.5.691","volume":"1","author":"H. J. Ohlbach","year":"1991","unstructured":"Ohlbach, H. J. (1991), Semantics based translation methods for modal logics, Journal of Logic and Computation 1(5), 691\u2013746.","journal-title":"Journal of Logic and Computation"},{"issue":"5","key":"9_CR14","doi-asserted-by":"publisher","first-page":"581","DOI":"10.1093\/logcom\/7.5.581","volume":"7","author":"H. J. Ohlbach","year":"1997","unstructured":"Ohlbach, H. J. and Schmidt, R. A. (1997), Functional translation and second-order frame properties of modal logics, Journal of Logic and Computation 7(5), 581\u2013603.","journal-title":"Journal of Logic and Computation"},{"key":"9_CR15","first-page":"73","volume-title":"Machine Intelligence 7","author":"G. Plotkin","year":"1972","unstructured":"Plotkin, G. (1972), Building-in equational theories, in B. Meltzer and D. Michie (eds), Machine Intelligence 7, American Elsevier, New York, pp. 73\u201390."},{"key":"9_CR16","volume-title":"Research Report MPI-I-98-2-003","author":"R. A. Schmidt","year":"1998","unstructured":"Schmidt, R. A. (1998), E-unification for subsystems of S4, Research Report MPI-I-98-2-003, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany."},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Schulz, K. U. (1992), Makanin's algorithm for word equations: Two improvements and a generalization, in K. U. Schulz (ed.), Word Equations and Related Topics, Vol. 572 of LNCS, Springer, pp. 85\u2013150.","DOI":"10.1007\/3-540-55124-7_4"},{"issue":"9","key":"9_CR18","first-page":"22","volume":"33","author":"N. K. Zamov","year":"1989","unstructured":"Zamov, N. K. (1989), Modal resolutions, Soviet Mathematics 33(9), 22\u201329. Translated from Izv. Vyssh. Uchebn. Zaved. Mat. 9 (328) (1989) 22\u201329.","journal-title":"Soviet Mathematics"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0052364","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,4]],"date-time":"2024-02-04T18:32:01Z","timestamp":1707071521000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0052364"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540643012","9783540697213"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/bfb0052364","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}