{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T17:31:29Z","timestamp":1777915889592,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540440390","type":"print"},{"value":"9783540456858","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45685-6_10","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T16:47:53Z","timestamp":1179593273000},"page":"131-147","source":"Crossref","is-referenced-by-count":14,"title":["Formalised Cut Admissibility for Display Logic"],"prefix":"10.1007","author":[{"given":"Jeremy E.","family":"Dawson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rajeev","family":"Gor\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,25]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/BF00284976","volume":"11","author":"N. D. Belnap","year":"1982","unstructured":"N D Belnap. Display logic. Journal of Philosophical Logic, 11:375\u2013417, 1982.","journal-title":"Journal of Philosophical Logic"},{"key":"10_CR2","unstructured":"Jeremy E Dawson and R Gor\u00e9. Embedding display calculi into logical frameworks: Comparing Twelf and Isabelle. In C Fidge (Ed), Proc. CATS 2001: The Australian Theory Symposium, ENTCS, 42: 89\u2013103, 2001, Elsevier."},{"key":"10_CR3","unstructured":"J E. Dawson and R Gore. A new machine-checked proof of strong normalisation for display logic. Submitted 2001."},{"key":"10_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1007\/3-540-63172-0_40","volume-title":"CSL\u201996: Selected Papers of the Annual Conference of the European Association for Computer Science Logic","author":"R. Gor\u00e9","year":"1997","unstructured":"R Gor\u00e9. Cut-free display calculi for relation algebras. In D van Dalen and M Bezem (Eds), CSL\u201996: Selected Papers of the Annual Conference of the European Association for Computer Science Logic, LNCS 1258:198\u2013210. Springer, 1997."},{"issue":"3","key":"10_CR5","first-page":"451","volume":"6","author":"R. Gor\u00e9","year":"1998","unstructured":"R Gor\u00e9. Substructural logics on display. Logic Journal of the Interest Group in Pure and Applied Logic, 6(3):451\u2013504, 1998.","journal-title":"Logic Journal of the Interest Group in Pure and Applied Logic"},{"key":"10_CR6","unstructured":"J Harrison. Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI International Cambridge Computer Science Research Centre, 1995."},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"S Matthews. Implementing FS0 in Isabelle: adding structure at the metalevel. In J Calmet and C Limongelli, editors, Proc. Disco\u201996. Springer, 1996.","DOI":"10.1007\/3-540-61697-7_24"},{"key":"10_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/BFb0055143","volume-title":"Theorem Proving in Higher-Order Logics","author":"A. Mikhajlova","year":"1998","unstructured":"A Mikhajlova and J von Wright. Proving isomorphism of first-order proof systems in HOL. In J Grundy and M Newey, editors, Theorem Proving in Higher-Order Logics, LNCS 1479:295\u2013314. Springer, 1998."},{"key":"10_CR9","unstructured":"F Pfenning. Structural cut elimination. In Proc. LICS 94, 1994."},{"key":"10_CR10","series-title":"PhD thesis","volume-title":"Automating the Meta Theory of Deductive Systems","author":"C. Sch\u00fcrmann","year":"2000","unstructured":"C Sch\u00fcrmann. Automating the Meta Theory of Deductive Systems. PhD thesis, Dept. of Comp. Sci., Carnegie Mellon University, USA, CMU-CS-00-146, 2000."},{"key":"10_CR11","series-title":"Trends in Logic","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-1280-4","volume-title":"Displaying Modal Logic","author":"H. Wansing","year":"1998","unstructured":"H Wansing. Displaying Modal Logic, volume 3 of Trends in Logic. Kluwer Academic Publishers, Dordrecht, August 1998."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45685-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,22]],"date-time":"2020-04-22T01:38:27Z","timestamp":1587519507000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45685-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440390","9783540456858"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-45685-6_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}