{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T17:07:10Z","timestamp":1694624830721},"reference-count":10,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2005,11,10]],"date-time":"2005-11-10T00:00:00Z","timestamp":1131580800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2005,11,10]],"date-time":"2005-11-10T00:00:00Z","timestamp":1131580800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Arch. Math. Logic"],"published-print":{"date-parts":[[2006,3]]},"DOI":"10.1007\/s00153-005-0314-y","type":"journal-article","created":{"date-parts":[[2005,11,10]],"date-time":"2005-11-10T11:14:15Z","timestamp":1131621255000},"page":"357-364","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["A semantical proof of the strong normalization theorem for full propositional classical natural deduction"],"prefix":"10.1007","volume":"45","author":[{"given":"Karim","family":"Nour","sequence":"first","affiliation":[]},{"given":"Khelifa","family":"Saber","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,11,10]]},"reference":[{"key":"314_CR1","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/S0168-0072(02)00051-9","volume":"119","author":"Andou","year":"2003","unstructured":"Andou, Y.: Church-Rosser property of simple reduction for full first-order classical natural deduction. Ann. Pure Appl. logic 119, 225\u2013237 (2003)","journal-title":"Ann. Pure Appl. logic"},{"key":"314_CR2","first-page":"27","volume":"12","author":"David","year":"2003","unstructured":"David, R., Nour, K.: A short proof of the strong normalization of the simply typed \u03bb \u03bc-calculus. Schedae Informaticae 12, 27\u201333 (2003)","journal-title":"Schedae Informaticae"},{"key":"314_CR3","doi-asserted-by":"publisher","first-page":"1277","DOI":"10.2178\/jsl\/1067620187","volume":"68","author":"David","year":"4","unstructured":"David, R., Nour, K.: A short proof of the Strong Normalization of Classical Natural Deduction with Disjunction. J. symbo. Logic 68 (4), 1277\u20131288 (2003)","journal-title":"J. symbo. Logic"},{"key":"314_CR4","unstructured":"Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and types. Cambridge University Press, 1986"},{"key":"314_CR5","doi-asserted-by":"crossref","unstructured":"de Groote, P.: Strong normalization of classical natural deduction with disjunction. In 5th International Conference on typed lambda calculi and applications, TLCA'01. LNCS, 2044, Springer Verlag, 2001, pp. 182-196","DOI":"10.1007\/3-540-45413-6_17"},{"key":"314_CR6","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/s00153-002-0156-9","volume":"42","author":"Joachimski","year":"2003","unstructured":"Joachimski, F., Matthes, R.: Short proofs of normalization for the simply-typed lambda-calculus, permutative conversions and G\u00f6del's T. Archive for Mathematical Logic 42, 59\u201387 (2003)","journal-title":"Archive for Mathematical Logic"},{"key":"314_CR7","unstructured":"Matthes, R.: Non-strictly positive fixed-points for classical natural deduction. Manuscript, 2003"},{"key":"314_CR8","unstructured":"Nour, K., Saber, K.: Church-Russer property of full propositional classical natural deduction. Manuscript, 2004"},{"key":"314_CR9","doi-asserted-by":"crossref","unstructured":"Parigot, M.: \u03bb \u03bc-calculus: An algorithm interpretation of classical natural deduction. Lecture Notes in Artificial Intelligence (624), Springer Verlag 1992, pp. 190\u2013201","DOI":"10.1007\/BFb0013061"},{"key":"314_CR10","doi-asserted-by":"publisher","first-page":"1461","DOI":"10.2307\/2275652","volume":"62","author":"Parigot","year":"4","unstructured":"Parigot, M.: Proofs of strong normalization for second order classical natural deduction. J. Symbo. Logic 62 (4), 1461\u20131479 (1997)","journal-title":"J. Symbo. Logic"}],"container-title":["Archive for Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-005-0314-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00153-005-0314-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-005-0314-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-005-0314-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,14]],"date-time":"2022-05-14T00:03:35Z","timestamp":1652486615000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00153-005-0314-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,11,10]]},"references-count":10,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2006,3]]}},"alternative-id":["314"],"URL":"https:\/\/doi.org\/10.1007\/s00153-005-0314-y","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"value":"0933-5846","type":"print"},{"value":"1432-0665","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,11,10]]},"assertion":[{"value":"12 November 2004","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 November 2005","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}