{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T01:22:47Z","timestamp":1755220967893,"version":"3.43.0"},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2002,10,1]],"date-time":"2002-10-01T00:00:00Z","timestamp":1033430400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,10,1]],"date-time":"2002-10-01T00:00:00Z","timestamp":1033430400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Studia Logica"],"published-print":{"date-parts":[[2002,10]]},"DOI":"10.1023\/a:1020526008642","type":"journal-article","created":{"date-parts":[[2003,3,18]],"date-time":"2003-03-18T15:12:43Z","timestamp":1048000363000},"page":"31-59","source":"Crossref","is-referenced-by-count":0,"title":["Simultaneous Rigid Sorted Unification for Tableaux"],"prefix":"10.1007","volume":"72","author":[{"given":"P. J.","family":"Mart\u00edn","sequence":"first","affiliation":[]},{"given":"A.","family":"Gavilanes","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5106685_CR1","first-page":"113","volume":"3","author":"A. G. Cohn","year":"1987","unstructured":"Cohn, A. G., A more expressive formulation of many sorted logic, Journal of Automated Reasoning 3, 113-200, 1987.","journal-title":"Journal of Automated Reasoning"},{"key":"5106685_CR2","doi-asserted-by":"crossref","unstructured":"Cohn, A. G., A many sorted logic with possibly empty sorts, CADE'11, LNCS 607, 633-647, 1992.","DOI":"10.1007\/3-540-55602-8_197"},{"issue":"1","key":"5106685_CR3","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1023\/A:1005996623714","volume":"20","author":"A. Degtyarev","year":"1998","unstructured":"Degtyarev, A., and A. Voronkov, What you always wanted to know about rigid E-unification, Journal of Automated Reasoning 20(1), 47-80, 1998.","journal-title":"Journal of Automated Reasoning"},{"key":"5106685_CR4","doi-asserted-by":"crossref","unstructured":"D'Agostino, M., D. Gabbay, R. H\u00c4hnle, and J. Posegga, Handbook of tableau methods, Kluwer Academic Publishers, 1999.","DOI":"10.1007\/978-94-017-1754-0"},{"key":"5106685_CR5","doi-asserted-by":"crossref","unstructured":"Fitting, M., First-Order Logic and Automated Theorem Proving (2 edition), Springer, 1996.","DOI":"10.1007\/978-1-4612-2360-3"},{"key":"5106685_CR6","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1016\/0004-3702(91)90009-9","volume":"49","author":"A. M. Frisch","year":"1991","unstructured":"Frisch, A. M., The substitutional framework for sorted deduction: fundamental results on hybrid reasoning, Artificial Intelligence 49, 161-198, 1991.","journal-title":"Artificial Intelligence"},{"key":"5106685_CR7","doi-asserted-by":"crossref","unstructured":"Gavilanes, A., J. Leach, P. J. Mart\u00cdn, and S. Nieva, Reasoning with preorders and dynamic sorts using free variable tableaux, AISMC-3, LNCS 1138, 365-379, 1996.","DOI":"10.1007\/3-540-61732-9_69"},{"key":"5106685_CR8","unstructured":"Gavilanes, A., J. Leach, P. J. Mart\u00cdn, and S. Nieva, Semantic tableaux for a logic with preorders and dynamic declarations, TABLEAUX'97 (Position paper), CRIN 97-R-030, 7-12, 1997."},{"key":"5106685_CR9","unstructured":"Herzog, O., et al., LILOG-Linguistic and logic methods for the computational understanding of german, LILOG-Report 1b, IBM Germany, 1986."},{"key":"5106685_CR10","doi-asserted-by":"crossref","unstructured":"Kogel, E., Rigid E-unification simplified, TABLEAUX'95, LNCS 918, 17-30, 1995.","DOI":"10.1007\/3-540-59338-1_25"},{"key":"5106685_CR11","doi-asserted-by":"crossref","unstructured":"Lassez, J. L., M. J. Maher, and K. Marriot, Unification revisited, LNCS 306, 67-113, Springer Verlag, 1986.","DOI":"10.1007\/3-540-19129-1_4"},{"key":"5106685_CR12","doi-asserted-by":"crossref","unstructured":"Mart\u00cdn, P. J., A. Gavilanes, and J. Leach, Free variable tableaux for a logic with term declarations, TABLEAUX'98, LNAI 1397, 202-216. 1998.","DOI":"10.1007\/3-540-69778-0_23"},{"key":"5106685_CR13","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1006\/jsco.1999.0364","volume":"29","author":"P. J. Mart\u00cdn","year":"2000","unstructured":"Mart\u00cdn, P. J., A. Gavilanes, and J. Leach, Tableau methods for a logic with term declarations, Journal of Symbolic Computation 29, 343-372, 2000.","journal-title":"Journal of Symbolic Computation"},{"key":"5106685_CR14","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1006\/jsco.1995.1020","volume":"19","author":"R. Nieuwenhuis","year":"1995","unstructured":"Nieuwenhuis, R., and A. Rubio, Theorem proving with ordering and equality constrained clauses, Journal of Symbolic Computation 19, 321-351, 1995.","journal-title":"Journal of Symbolic Computation"},{"key":"5106685_CR15","doi-asserted-by":"crossref","unstructured":"Schmidt-Schauss, M., Computational Aspects of an Order Sorted Logic with Term Declarations, LNAI 395, Springer, 1989.","DOI":"10.1007\/BFb0024065"},{"key":"5106685_CR16","doi-asserted-by":"crossref","unstructured":"Walther, C., A Many-sorted Calculus based on Resolution and Paramodulation, Research Notes in Artificial Intelligence, Pitman, 1987.","DOI":"10.1016\/B978-0-273-08718-2.50007-9"},{"key":"5106685_CR17","unstructured":"Weidenbach, C., A sorted logic using dynamic sorts, MPI-I-91-218, 1991."},{"issue":"6","key":"5106685_CR18","first-page":"887","volume":"3","author":"C. Weidenbach","year":"1995","unstructured":"Weidenbach, C., First-order tableaux with sorts, Journal of the Interest Group in Pure and Applied Logics 3(6), 887-907, 1995.","journal-title":"Journal of the Interest Group in Pure and Applied Logics"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1020526008642.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1020526008642\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1020526008642.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T05:21:25Z","timestamp":1754630485000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1020526008642"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,10]]},"references-count":18,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2002,10]]}},"alternative-id":["5106685"],"URL":"https:\/\/doi.org\/10.1023\/a:1020526008642","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[2002,10]]}}}