{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:22:52Z","timestamp":1725664972647},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540612087"},{"type":"electronic","value":"9783540683681"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61208-4_6","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:19:12Z","timestamp":1330291152000},"page":"80-92","source":"Crossref","is-referenced-by-count":1,"title":["Cyclic connections"],"prefix":"10.1007","author":[{"given":"G\u00e9rard","family":"Becher","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"issue":"2","key":"6_CR1","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P. Andrews","year":"1981","unstructured":"P. Andrews. Theorem Proving via General Matings. J.ACM, 28(2):193\u2013214, 1981.","journal-title":"J.ACM"},{"key":"6_CR2","unstructured":"L. Bachmair and H. Ganzinger. Rewrite techniques for transitive relations. Technical Report MPI-I-93-249, Max-Planck-Institut f\u00fcr Informatik, 1993."},{"key":"6_CR3","unstructured":"G. Becher. D\u00e9monstration Automatique en Logique Temporelle et Algorithmes d'E-Unification Rigide. PhD thesis, Universit\u00e9 de Caen, 1995."},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"G. Becher and U. Petermann. Rigid Unification by Completion and Rigid Paramodulation. In B. Nebel and L. Dreschler-Fischer, editors, KI-94: Advances in Artificial Intelligence, volume 861 of Lecture Notes in Computer Science, pages 319\u2013330. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58467-6_28"},{"key":"6_CR5","volume-title":"Master's thesis","author":"B. Beckert","year":"1993","unstructured":"B. Beckert. Ein vervollst\u00e4ndigungsbasiertes Verfahren zur Behandlung von Gleichheit im Tableaukalk\u00fcl mit freien Variablen. Master's thesis, Universit\u00e4t Karlsruhe (TH), 1993."},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"W. Bibel. Automated Theorem Proving. Vieweg, 1st edition, 1982.","DOI":"10.1007\/978-3-322-90100-2"},{"key":"6_CR7","first-page":"70","volume-title":"Variable Elimination and Chaining in a Resolutionbased Prover for Inequalities","author":"W. Bledsoe","year":"1980","unstructured":"W. Bledsoe and L. Hines. Variable Elimination and Chaining in a Resolutionbased Prover for Inequalities. In S. Verlag, editor, Proc. 5th Conference on Automated Deduction, pages 70\u201387, Les Arcs, France, 1980."},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"A. Degtyarev and A. Voronkov. Simultaneous Rigid E-Unification is Undecidable. Technical report, Tech. Report No. 105. Computing Science Department, Uppsala University, May 1995.","DOI":"10.1007\/3-540-61377-3_38"},{"issue":"2","key":"6_CR9","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1145\/128749.128754","volume":"39","author":"J. Gallier","year":"1992","unstructured":"J. Gallier, P. Narendran, S. Raatz, and W. Snyder. Theorem Proving with Equational Matings and Rigid E-Unification. Journal of ACM, 39(2):377\u2013429, April 1992.","journal-title":"Journal of ACM"},{"key":"6_CR10","unstructured":"J. H. Gallier. Unification Procedures in Automated Deduction Methods Based on Matings: a Survey. In M. Nivat and A. Podelski, editors, Tree Automata and Languages, pages 439\u2013485. North-Holland Publishing Company, 1992."},{"key":"6_CR11","unstructured":"J. Goubault. A Rule-Based Algorithm for Rigid E-Unification. In G. Gottlob, A. Leitsch, and D. Mundici, editors, 3rd Kurt G\u00f6del Colloquium '93, volume 713 of Lecture Notes in Computer Science. Springer-Verlag, 1993."},{"key":"6_CR12","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/BF00263449","volume":"8","author":"L. M. Hines","year":"1992","unstructured":"L. M. Hines. Completeness of a Prover for Dense Linear Orders. Journal of Automated Reasoning, 8:45\u201375, 1992.","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"6_CR13","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"G. Nelson and D. C. Oppen. Fast Decision Procedures Based on Congruence Closure. Journal of Association for Computer Machinery, 27(2):356\u2013364, April 1980.","journal-title":"Journal of Association for Computer Machinery"},{"issue":"2","key":"6_CR14","first-page":"105","volume":"11","author":"U. Petermann","year":"1992","unstructured":"U. Petermann. How to build in an open theory into connection calculi. J. on Computer and Artificial Intelligence, 11(2):105\u2013142, 1992.","journal-title":"J. on Computer and Artificial Intelligence"},{"key":"6_CR15","unstructured":"U. Petermann. A complete equational connection calculus with rigid E-unification. NTZ-Report 26\/1993, Naturwissenschaftlich-Theoretisches Zentrum der Universit\u00e4t Leipzig, 1993."},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"M. E. Stickel. Automated deduction by theory resolution. Journal of Automated Reasoning, pages 333\u2013356, 1985.","DOI":"10.1007\/BF00244275"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61208-4_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:04:27Z","timestamp":1605647067000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61208-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540612087","9783540683681"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-61208-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}