{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T12:10:26Z","timestamp":1737288626544,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540660866"},{"type":"electronic","value":"9783540487548"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48754-9_19","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T16:20:56Z","timestamp":1184602856000},"page":"202-216","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Simple Sequent System for First-Order Logic with Free Constructors"],"prefix":"10.1007","author":[{"given":"Jean","family":"Goubault-Larrecq","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,2,11]]},"reference":[{"key":"19_CR1","unstructured":"B. Barras, S. Boutin, C. Cornes, J. Courant, J.-C. Filli\u00e2tre, E. Gim\u00e9nez, H. Herbelin, G. Huet, C. Mu\u00f1oz, C. Murthy, C. Parent, C. Paulin, A. Sa\u00efbi, and B. Werner. The Coq proof assistant reference manual \u2014 version V6.1. Technical Report 0203, INRIA, 1997."},{"key":"19_CR2","unstructured":"P. Baumgartner. A predicative encoding of equality. Slides available at http:\/\/www.uni-koblenz.de\/~peter\/DFG-Impl-Equality.ps.gz ."},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"D. Bolignano. Formal verification of cryptographic protocols. In 3rd ACM Conf. on Computer and Communication Security, 1996.","DOI":"10.1145\/238168.238196"},{"key":"19_CR4","unstructured":"H. Comon. Disunification: a survey. In Computational Logic: Essays in Honor of Alan Robinson. MIT Press, 1991."},{"key":"19_CR5","unstructured":"J.-Y. Girard. A fixpoint theorem in linear logic. Note on the linear logic mailing list, http:\/\/www.csl.sri.com\/linear\/mailing-list-traffic\/www\/07\/mail_3.html , 1992."},{"key":"19_CR6","unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989."},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"J. Goubault-Larrecq. A simple deduction system for first-order logic with equality, free constructors and induction. Research report, INRIA, March 1999.","DOI":"10.1007\/3-540-48754-9_19"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"J. Goubault-Larrecq and I. Mackie. Proof Theory and Automated Deduction, volume 6 of Applied Logic Series. Kluwer, 1997.","DOI":"10.1007\/978-94-011-3981-6"},{"key":"19_CR9","unstructured":"R. Harper, R. Milner, and M. Tofte. The Definition of Standard ML. MIT Press, 1990."},{"issue":"2","key":"19_CR10","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"A. Martelli and U. Montanari. An efficient unification algorithm. ACM Trans. Prog. Lang. Sys., 4(2):258\u2013282, 1982.","journal-title":"ACM Trans. Prog. Lang. Sys."},{"key":"19_CR11","doi-asserted-by":"publisher","first-page":"29","DOI":"10.2307\/1996581","volume":"177","author":"R. Parikh","year":"1973","unstructured":"R. Parikh. Some results on the lengths of proofs. Trans. AMS, 177:29\u201336, 1973.","journal-title":"Trans. AMS"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"L. Paulson. Proving properties of security protocols by induction. In IEEE Computer Security Foundations Workshop X, pages 70\u201383, 1997.","DOI":"10.1109\/CSFW.1997.596788"},{"key":"19_CR13","first-page":"73","volume":"7","author":"G. Plotkin","year":"1972","unstructured":"G. Plotkin. Building in equational theories. Machine Intelligence, 7:73\u201390, 1972.","journal-title":"Machine Intelligence"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"M. E. Stickel. Automated deduction by theory resolution. In 9th IJCAI, pages 1181\u20131186, 1985.","DOI":"10.1007\/BF00244275"},{"issue":"1","key":"19_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/42267.45071","volume":"35","author":"C. Walther","year":"1988","unstructured":"C. Walther. Many-sorted unification. J. ACM, 35(1):1\u201317, 1988.","journal-title":"J. ACM"},{"key":"19_CR16","unstructured":"A. N. Whitehead and B. Russell. Principia Mathematica. Cambridge University Press, 1910, 1927."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48754-9_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T11:54:18Z","timestamp":1737287658000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48754-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540660866","9783540487548"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-48754-9_19","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"11 February 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}