{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:21Z","timestamp":1749125181775,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540631040"},{"type":"electronic","value":"9783540691402"}],"license":[{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"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":[[1997]]},"DOI":"10.1007\/3-540-63104-6_32","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:04:17Z","timestamp":1330297457000},"page":"321-335","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Soft typing for ordered resolution"],"prefix":"10.1007","author":[{"given":"Harald","family":"Ganzinger","sequence":"first","affiliation":[]},{"given":"Christoph","family":"Meyer","sequence":"additional","affiliation":[]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"32_CR1","unstructured":"Bachmair, L. and Ganzinger, H. [1991], Perfect model semantics for logic programs with equality, in \u2018Proc. International Conference on Logic Programming '91', MIT Press, pp. 645\u2013659."},{"issue":"3","key":"32_CR2","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L. and Ganzinger, H. [1994], \u2018Rewrite-based equational theorem proving with selection and simplification', Journal of Logic and Computation 4(3), 217\u2013247. Revised version of Max-Planck-Institut f\u00fcr Informatik technical report, MPI-I-91-208, 1991.","journal-title":"Journal of Logic and Computation"},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"Comon, H. [1995], Sequentiality, second order monadic logic and tree automata, in \u2018Proceedings 10th IEEE Symposium on Logic in Computer Science, LICS'95', IEEE Computer Society Press, pp. 508\u2013517.","DOI":"10.1109\/LICS.1995.523285"},{"key":"32_CR4","doi-asserted-by":"crossref","unstructured":"Fr\u00fchwirth, T., Shapiro, E., Vardi, M. Y. and Yardeni, E. [1991], Logic programs as types for logic programs, in A. R. Meyer, ed., \u2018Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science, LICS'91', IEEE Computer Society Press, pp. 300\u2013309.","DOI":"10.1109\/LICS.1991.151654"},{"key":"32_CR5","unstructured":"Jacquemard, F. [1996], Decidable approximations of term rewriting systems, in H. Ganzinger, ed., \u2018Rewriting Techniques and Applications, 7th International Conference, RTA-96', Vol. 1103 of LNCS, Springer, pp. 362\u2013376."},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"Manthey, R. and Bry, F. [1988], Satchmo: A theorem prover implemented in prolog, in E. Lusk and R. Overbeek, eds, \u20189th International Conference on Automated Deduction, CADE-9', Vol. 310 of LNCS, Springer, pp. 415\u2013434.","DOI":"10.1007\/BFb0012847"},{"key":"32_CR7","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R. [1996], Basic paramodulation and decidable theories (extended abstract), in \u2018Proceedings 11th IEEE Symposium on Logic in Computer Science, LICS'96', IEEE Computer Society Press, pp. 473\u2013482.","DOI":"10.1109\/LICS.1996.561464"},{"key":"32_CR8","volume-title":"Technical report","author":"D. A. Plaisted","year":"1994","unstructured":"Plaisted, D. A. [1994], Ordered semantic hyper-linking, Technical report, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken."},{"key":"32_CR9","volume-title":"Technical Report MPI-I-97-2-002","author":"R. A. Schmidt","year":"1997","unstructured":"Schmidt, R. A. [1997], Resolution is a decision procedure for many prepositional modal logics, Technical Report MPI-I-97-2-002, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany. The extended abstract version is to appear in Kracht, M., de Rijke, M., Wansing, H. and Zakharyaschev, M. (eds) (1997), Advances in Modal Logic '96, CSLI Publications, Stanford."},{"key":"32_CR10","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1145\/321420.321428","volume":"14","author":"J. R. Slagle","year":"1967","unstructured":"Slagle, J. R. [1967], \u2018Automatic theorem-proving with renamable and semantic resolution', Journal of the ACM 14, 687\u2013697.","journal-title":"Journal of the ACM"},{"key":"32_CR11","volume-title":"Dissertation","author":"C. Weidenbach","year":"1996","unstructured":"Weidenbach, C. [1996], Computational Aspects of a First-Order Logic with Sorts, Dissertation, Technische Fakult\u00e4t der Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany."},{"key":"32_CR12","unstructured":"Weidenbach, C., Gaede, B. and Rock, G. [1996], SPASS & FLOTTER, Version 0.42, in M. McRobbie and J. Slaney, eds, \u201813th International Conference on Automated Deduction, CADE-13', Vol. 1104 of LNAI, Springer, pp. 141\u2013145."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-14"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63104-6_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:36:29Z","timestamp":1742600189000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63104-6_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631040","9783540691402"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-63104-6_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]},"assertion":[{"value":"8 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}