{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:38:03Z","timestamp":1725471483489},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540659228"},{"type":"electronic","value":"9783540488552"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/10703163_26","type":"book-chapter","created":{"date-parts":[[2006,10,9]],"date-time":"2006-10-09T18:15:50Z","timestamp":1160417750000},"page":"385-398","source":"Crossref","is-referenced-by-count":9,"title":["RPO Constraint Solving Is in NP"],"prefix":"10.1007","author":[{"given":"Paliath","family":"Narendran","sequence":"first","affiliation":[]},{"given":"Michael","family":"Rusinowitch","sequence":"additional","affiliation":[]},{"given":"Rakesh","family":"Verma","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"Comon, H.: Solving inequations in term algebras. In: Proc. 5th IEEE Symp. Logic in Computer Science (LICS), Philadelphia (June 1990)","DOI":"10.1109\/LICS.1990.113734"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Comon, H., Treinen, R.: The first-order theory of lexicographic path orderings is undecidable. Theoretical Computer Science\u00a0176 (April 1997)","DOI":"10.1016\/S0304-3975(96)00049-7"},{"issue":"3","key":"26_CR3","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N.: Orderings for term-rewriting systems. Theoretical Computer Science\u00a017(3), 279\u2013301 (1982)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"26_CR4","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"Dershowitz, N.: Termination of rewriting. Journal of Symbolic Computation\u00a03(1), 69\u2013115 (1987)","journal-title":"Journal of Symbolic Computation"},{"key":"26_CR5","first-page":"243","volume-title":"Handbook of Theoretical Computer Science","author":"N. Dershowitz","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, pp. 243\u2013309. North-Holland, Amsterdam (1990)"},{"key":"26_CR6","unstructured":"Ganzinger, H., Nieuwenhuis, R., Nivela, P.: The Saturate System (1995), Software and documentation available from: \n                    \n                      http:\/\/www.mpi-sb.mpg.de"},{"key":"26_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/3-540-18088-5_6","volume-title":"Automata, Languages and Programming","author":"J. Hsiang","year":"1987","unstructured":"Hsiang, J., Rusinowitch, M.: On word problems in equational theories. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol.\u00a0267, pp. 54\u201371. Springer, Heidelberg (1987)"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1007\/3-540-54233-7_155","volume-title":"Automata, Languages and Programming","author":"J.-P. Jouannaud","year":"1991","unstructured":"Jouannaud, J.-P., Okada, M.: Satisfiability of systems of ordinal notations with the subterm ordering is decidable. In: Leach Albert, J., Monien, B., Rodr\u00edguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol.\u00a0510, pp. 455\u2013468. Springer, Heidelberg (1991)"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/3-540-15198-2_11","volume-title":"Mathematical Foundations of Software Development","author":"D. Kapur","year":"1985","unstructured":"Kapur, D., Narendran, P., Sivakumar, G.: A path ordering for proving termination of term rewriting systems. In: Nivat, M., Floyd, C., Thatcher, J., Ehrig, H. (eds.) CAAP 1985 and TAPSOFT 1985. LNCS, vol.\u00a0185, pp. 173\u2013187. Springer, Berlin (1985)"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"D. Kapur","year":"1995","unstructured":"Kapur, D., Sivakumar, G.: Maximal Extensions of Simplification Orderings. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol.\u00a01026. Springer, Heidelberg (1995)"},{"issue":"3","key":"26_CR11","first-page":"9","volume":"4","author":"C. Kirchner","year":"1990","unstructured":"Kirchner, C., Kirchner, H., Rusinowitch, M.: Deduction with symbolic constraints. Revue Fran\u00e7aise d\u2019Intelligence Artificielle\u00a04(3), 9\u201352 (1990) (Special issue on automatic deduction)","journal-title":"Revue Fran\u00e7aise d\u2019Intelligence Artificielle"},{"key":"26_CR12","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0304-3975(85)90175-6","volume":"40","author":"M.S. Krishnamoorthy","year":"1985","unstructured":"Krishnamoorthy, M.S., Narendran, P.: Note on recursive path ordering. TCS\u00a040, 323\u2013328 (1985)","journal-title":"TCS"},{"issue":"1","key":"26_CR13","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/BF00302640","volume":"6","author":"P. Lescanne","year":"1990","unstructured":"Lescanne, P.: On the recursive decomposition ordering with lexicographical status and other related orderings. J. of Automated Reasoning\u00a06(1), 39\u201349 (1990)","journal-title":"J. of Automated Reasoning"},{"issue":"2","key":"26_CR14","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/0020-0190(93)90226-Y","volume":"47","author":"R. Nieuwenhuis","year":"1993","unstructured":"Nieuwenhuis, R.: Simple LPO constraint solving methods. Inf. Process. Lett.\u00a047(2), 65\u201369 (1993)","journal-title":"Inf. Process. Lett."},{"key":"26_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1007\/3-540-55602-8_186","volume-title":"Automated Deduction - CADE-11","author":"R. Nieuwenhuis","year":"1992","unstructured":"Nieuwenhuis, R., Rubio, A.: Theorem proving with ordering constrained clauses. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 477\u2013491. Springer, Heidelberg (1992)"},{"key":"26_CR16","unstructured":"Plaisted, D.: A recursively defined ordering for proving termination of term rewriting systems. Technical Report R-78-943, U. of Illinois, Dept of Computer Science (1978)"},{"key":"26_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"434","DOI":"10.1007\/3-540-51081-8_124","volume-title":"Rewriting Techniques and Applications","author":"J. Steinbach","year":"1989","unstructured":"Steinbach, J.: Extensions and comparison of simplification orderings. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol.\u00a0355, pp. 434\u2013448. Springer, Heidelberg (1989)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10703163_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,15]],"date-time":"2019-03-15T08:20:19Z","timestamp":1552638019000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10703163_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540659228","9783540488552"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/10703163_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}