{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:23:00Z","timestamp":1725664980284},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540617327"},{"type":"electronic","value":"9783540707400"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61732-9_69","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:17:16Z","timestamp":1330276636000},"page":"365-379","source":"Crossref","is-referenced-by-count":3,"title":["Reasoning with preorders and dynamic sorts using free variable tableaux"],"prefix":"10.1007","author":[{"given":"A.","family":"Gavilanes","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.","family":"Leach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P. J.","family":"Mart\u00edn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Nieva","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"23_CR1","unstructured":"L. Bachmair, H. Ganzinger, Ordered Chaining Calculi for First-Order Theories of Binary Relations. MPI-I-95-2-009, 1995."},{"key":"23_CR2","first-page":"507","volume":"607","author":"B. Beckert","year":"1992","unstructured":"B. Beckert, R. H\u00e4hnle. An Improved Method for Adding Equality to Free Variable Semantic Tableaux. Proc. CADE'10. LNAI 607, 507\u2013521, 1992.","journal-title":"LNAI"},{"key":"23_CR3","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/0004-3702(85)90015-3","volume":"27","author":"W. W. Bledsoe","year":"1985","unstructured":"W. W. Bledsoe, K. Kunen, R. Shostak. Completeness Results for Inequality Provers. Artificial Intelligence 27, 255\u2013288, 1985.","journal-title":"Artificial Intelligence"},{"key":"23_CR4","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF00244394","volume":"4","author":"M. Fitting","year":"1988","unstructured":"M. Fitting. First-Order modal tableaux. J. of Automated Reasoning 4, 191\u2013213, 1988.","journal-title":"J. of Automated Reasoning"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"M. Fitting. First-Order Logic and Automated Theorem Proving. Second edition. Springer, 1996.","DOI":"10.1007\/978-1-4612-2360-3"},{"key":"23_CR6","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1016\/0304-3975(90)90005-3","volume":"74","author":"A. Gavilanes-Franco","year":"1990","unstructured":"A. Gavilanes-Franco, F. Lucio-Carrasco. A first order logic for partial functions. TCS 74, 37\u201369, 1990.","journal-title":"TCS"},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"A. Gavilanes, J. Leach, S. Nieva. Free Variable Tableaux for a Many Sorted Logic with Preorders. To appear in Proc. AMAST'96, Springer, 1996.","DOI":"10.1007\/BFb0014310"},{"key":"23_CR8","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1007\/3-540-61732-9_69","volume-title":"Artificial Intelligence and Symbolic Mathematical Computation","author":"A. Gavilanes","year":"1996","unstructured":"A. Gavilanes, J. Leach, P. J. Mart\u00edn, S. Nieva. Reasoning with Preorders and Dynamic Sorts using Free Variable Tableaux. Technical Report DIA 34\/96, Univ. Complutense de Madrid, 1996."},{"key":"23_CR9","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90302-V","volume":"105","author":"J. A. Goguen","year":"1992","unstructured":"J. A. Goguen, J. Meseguer. Order-sorted algebra I: Eguational deduction for multiple inheritance, overloading, exceptions and partial operations. TCS 105, 217\u2013273, 1992.","journal-title":"TCS"},{"key":"23_CR10","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/BF00881956","volume":"13","author":"R. H\u00e4hnle","year":"1994","unstructured":"R. H\u00e4hnle, P. H. Schmitt. The liberalized \u03b4-rule in free variable semantic tableaux. J. of Automated Reasoning 13, 211\u2013221, 1994.","journal-title":"J. of Automated Reasoning"},{"key":"23_CR11","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19\/20","author":"J. Jaffar","year":"1994","unstructured":"J. Jaffar, M. J. Maher. Constraint logic programming: A survey. J. of Logic Programming 19\/20, 503\u2013582, 1994.","journal-title":"J. of Logic Programming"},{"key":"23_CR12","first-page":"17","volume":"690","author":"J. Levy","year":"1993","unstructured":"J. Levy, J. Agust\u00ed. Bi-rewriting, a term rewriting technique for monotonie order relations. Proc. RTA'93. LNCS 690, 17\u201331, 1993.","journal-title":"LNCS"},{"issue":"1","key":"23_CR13","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1080\/11663081.1993.10510794","volume":"3","author":"J. Leach","year":"1993","unstructured":"J. Leach, S. Nieva. Foundations of a Theorem Prover for Functional and Mathematical Uses. J. of Applied Non-Classical Logics 3(1), 7\u201338, 1993.","journal-title":"J. of Applied Non-Classical Logics"},{"key":"23_CR14","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/BF00244513","volume":"4","author":"F. Oppacher","year":"1988","unstructured":"F. Oppacher, E. Suen. HARP: A Tableau-Based Theorem Prover. J. of Automated Reasoning 4, 69\u2013100, 1988.","journal-title":"J. of Automated Reasoning"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"M. Schmidt-Schauss. Computational aspects of an order sorted logic with term declarations. LNAI 395. Springer,1989.","DOI":"10.1007\/BFb0024065"},{"key":"23_CR16","first-page":"49","volume":"418","author":"P.H. Schmitt","year":"1990","unstructured":"P.H. Schmitt, W. Wernecke. Tableau Calculus for Order Sorted Logic. Proc. Workshop on Sorts and Types in Artificial Intelligence (1989). LNAI 418, 49\u201360, 1990.","journal-title":"LNAI"},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"C. Walther. 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":"23_CR18","first-page":"18","volume":"418","author":"C. Walther","year":"1990","unstructured":"C. Walther. Many Sorted Inferences in Automated Theorem Proving. Proc. Workshop on Sorts and Types in Artificial Intelligence (1989). LNAI 418, 18\u201348, 1990.","journal-title":"LNAI"},{"key":"23_CR19","unstructured":"C. Weidenbach. A sorted logic using dynamic sorts. MPI-I-91-218, 1991."},{"issue":"6","key":"23_CR20","first-page":"887","volume":"3","author":"C. Weidenbach","year":"1995","unstructured":"C. Weidenbach. First-Order Tableaux with Sorts. J. of the Interest Group in Pure and Applied Logics 3(6), 887\u2013907, 1995.","journal-title":"J. of the Interest Group in Pure and Applied Logics"},{"key":"23_CR21","doi-asserted-by":"crossref","unstructured":"C. Weidenbach. Unification in Sort Theories and its Applications. Annals of Mathematics and Artificial Intelligence. To appear.","DOI":"10.1007\/BF02127750"}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Mathematical Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61732-9_69.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:09:53Z","timestamp":1605629393000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61732-9_69"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540617327","9783540707400"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-61732-9_69","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}