{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:51:26Z","timestamp":1725475886846},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676973"},{"type":"electronic","value":"9783540450085"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722086_25","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T19:43:15Z","timestamp":1167421395000},"page":"309-323","source":"Crossref","is-referenced-by-count":0,"title":["Monotonic Preorders for Free Variable Tableaux"],"prefix":"10.1007","author":[{"given":"Pedro J.","family":"Mart\u00edn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antonio","family":"Gavilanes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"25_CR1","first-page":"384","volume-title":"Rewrite techniques for transitive relations. Procs. LICS 1994","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite techniques for transitive relations. In: Procs. LICS 1994, pp. 384\u2013393. IEEE Computer Science Press, Los Alamitos (1994)"},{"key":"25_CR2","series-title":"LNAI","first-page":"462","volume-title":"Automated Deduction - CADE-11","author":"L. Bachmair","year":"1992","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation and su- perposition. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol.\u00a0607, pp. 462\u2013476. Springer, Heidelberg (1992)"},{"key":"25_CR3","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1006\/inco.1995.1131","volume":"121","author":"L. Bachmair","year":"1995","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic paramodulation. Information and Computation\u00a0121, 172\u2013192 (1995)","journal-title":"Information and Computation"},{"issue":"1","key":"25_CR4","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1023\/A:1005996623714","volume":"20","author":"A. Degtyarev","year":"1998","unstructured":"Degtyarev, A., Voronkov, A.: What you always wanted to know about rigid E- unification. Journal of Automated Reasoning\u00a020(1), 47\u201380 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"25_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M. Fitting","year":"1996","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, Heidelberg (1996)","edition":"2"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","first-page":"7","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"A. Gavilanes","year":"1997","unstructured":"Gavilanes, A., Leach, J., Mart\u00edn, P.J., Nieva, S.: Semantic Tableaux for a Logic with Preorders and Dynamic Declarations. In: Galmiche, D. (ed.) TABLEAUX 1997. LNCS, vol.\u00a01227, pp. 7\u201312. Springer, Heidelberg (1997)"},{"issue":"1\/2","key":"25_CR7","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/0890-5401(90)90061-L","volume":"87","author":"J. Gallier","year":"1990","unstructured":"Gallier, J., Narendran, P., Plaisted, D., Snyder, W.: Rigid E-unification: NP- completeness and applications to equational matings. Information and Computation\u00a087(1\/2), 129\u2013195 (1990)","journal-title":"Information and Computation"},{"key":"25_CR8","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1006\/jsco.1996.0053","volume":"22","author":"J. Levy","year":"1996","unstructured":"Levy, J., Agust\u00ed, J.: Bi-rewrite systems. J. Symbolic Computation\u00a022, 279\u2013314 (1996)","journal-title":"J. Symbolic Computation"},{"key":"25_CR9","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1006\/jsco.1995.1020","volume":"19","author":"R. Nieuwenhuis","year":"1995","unstructured":"Nieuwenhuis, R., Rubio, A.: Theorem Proving with Ordering and Equality Constrained Clauses. J. Symbolic Computation\u00a019, 321\u2013351 (1995)","journal-title":"J. Symbolic Computation"},{"key":"25_CR10","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. Information Processing Letters\u00a047, 65\u201369 (1993)","journal-title":"Information Processing Letters"},{"key":"25_CR11","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/S0747-7171(08)80131-9","volume":"11","author":"M. Rusinowitch","year":"1991","unstructured":"Rusinowitch, M.: Theorem proving with resolution and superposition. J. Symbolic Computation\u00a011, 21\u201349 (1991)","journal-title":"J. Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722086_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T05:24:26Z","timestamp":1553318666000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722086_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676973","9783540450085"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/10722086_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}