{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:00:20Z","timestamp":1725487220211},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540727323"},{"type":"electronic","value":"9783540727347"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-72734-7_24","type":"book-chapter","created":{"date-parts":[[2007,6,28]],"date-time":"2007-06-28T09:40:50Z","timestamp":1183023650000},"page":"332-348","source":"Crossref","is-referenced-by-count":0,"title":["Proof Identity for Classical Logic: Generalizing to Normality"],"prefix":"10.1007","author":[{"given":"Roman","family":"Kuznets","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"8","key":"24_CR1","doi-asserted-by":"publisher","first-page":"801","DOI":"10.1109\/TC.1976.1674698","volume":"25","author":"P.B. Andrews","year":"1976","unstructured":"Andrews, P.B.: Refutations by matings. IEEE Transactions on Computers\u00a025(8), 801\u2013807 (1976)","journal-title":"IEEE Transactions on Computers"},{"key":"24_CR2","unstructured":"Artemov, S.N.: Operational modal logic. Technical Report MSI 95\u201329, Cornell University (1995)"},{"issue":"1","key":"24_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/2687821","volume":"7","author":"S.N. Artemov","year":"2001","unstructured":"Artemov, S.N.: Explicit provability and constructive semantics. Bulletin of Symbolic Logic\u00a07(1), 1\u201336 (2001)","journal-title":"Bulletin of Symbolic Logic"},{"key":"24_CR4","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/0304-3975(79)90054-9","volume":"8","author":"W. Bibel","year":"1979","unstructured":"Bibel, W.: Tautology testing with a generalized matrix reduction method. Theoretical Computer Science\u00a08, 31\u201344 (1979)","journal-title":"Theoretical Computer Science"},{"key":"24_CR5","first-page":"909","volume-title":"Information Processing 83","author":"J. Corbin","year":"1983","unstructured":"Corbin, J., Bidoit, M.: A rehabilitation of Robinson\u2019s unification algorithm. In: Mason, R.E.A. (ed.) Information Processing 83, pp. 909\u2013914. North-Holland, Amsterdam (1983)"},{"issue":"1","key":"24_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.apal.2004.04.009","volume":"132","author":"M. Fitting","year":"2005","unstructured":"Fitting, M.: The Logic of Proofs, semantically. Annals of Pure and Applied Logic\u00a0132(1), 1\u201325 (2005)","journal-title":"Annals of Pure and Applied Logic"},{"key":"24_CR7","unstructured":"Fitting, M.: Realizing substitution instances of modal theorems. Unpublished (2006), available at http:\/\/comet.lehman.cuny.edu\/fitting\/"},{"key":"24_CR8","first-page":"86","volume-title":"Kurt G\u00f6del Collected Works, vol. III","author":"K. G\u00f6del","year":"1995","unstructured":"G\u00f6del, K.: Vortrag bei Zilsel (*1938a). In: Feferman, S., Dawson Jr., J.W., Goldfarb, W., Parsons, C., Solovay, R.N. (eds.) Kurt G\u00f6del Collected Works, vol. III, pp. 86\u2013113. Oxford University Press, Oxford (1995)"},{"key":"24_CR9","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Proofs and Types","author":"J.-Y. Girard","year":"1989","unstructured":"Girard, J.-Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol.\u00a07. Cambridge University Press, Cambridge (1989)"},{"key":"24_CR10","doi-asserted-by":"publisher","first-page":"29","DOI":"10.2307\/1995158","volume":"146","author":"R. Hindley","year":"1969","unstructured":"Hindley, R.: The principal type-scheme of an object in combinatory logic. Transactions of the American Mathematical Society\u00a0146, 29\u201360 (1969)","journal-title":"Transactions of the American Mathematical Society"},{"issue":"1\u20133","key":"24_CR11","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1016\/j.tcs.2006.03.015","volume":"357","author":"N.V. Krupski","year":"2006","unstructured":"Krupski, N.V.: On the complexity of the reflected logic of proofs. Theoretical Computer Science\u00a0357(1\u20133), 136\u2013142 (2006)","journal-title":"Theoretical Computer Science"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/3-540-44622-2_25","volume-title":"Computer Science Logic","author":"R. Kuznets","year":"2000","unstructured":"Kuznets, R.: On the complexity of explicit modal logics. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol.\u00a01862, pp. 371\u2013383. Springer, Heidelberg (2000)"},{"issue":"4","key":"24_CR13","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/BF01703261","volume":"2","author":"J. Lambek","year":"1968","unstructured":"Lambek, J.: Deductive systems and categories I. Syntactic calculus and residuated categories. Mathematical Systems Theory\u00a02(4), 287\u2013318 (1968)","journal-title":"Mathematical Systems Theory"},{"key":"24_CR14","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/BFb0079385","volume-title":"Category Theory, Homology Theory and their Applications I","author":"J. Lambek","year":"1969","unstructured":"Lambek, J.: Deductive systems and categories II. Standard constructions and closed categories. In: Category Theory, Homology Theory and their Applications I. Lecture Notes in Mathematics, vol.\u00a086, pp. 76\u2013122. Springer, Heidelberg (1969)"},{"key":"24_CR15","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/BFb0073965","volume-title":"Toposes, Algebraic Geometry and Logic","author":"J. Lambek","year":"1972","unstructured":"Lambek, J.: Deductive systems and categories III. Cartesian closed categories, intuitionist propositional calculus, and combinatory logic. In: Toposes, Algebraic Geometry and Logic. Lecture Notes in Mathematics, vol.\u00a0274, pp. 57\u201382. Springer, Heidelberg (1972)"},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/11417170_19","volume-title":"Typed Lambda Calculi and Applications","author":"F. Lamarche","year":"2005","unstructured":"Lamarche, F., Stra\u00dfburger, L.: Naming proofs in classical propositional logic. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 246\u2013261. Springer, Heidelberg (2005)"},{"issue":"3","key":"24_CR17","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/j.apal.2006.03.001","volume":"145","author":"R. Milnikel","year":"2007","unstructured":"Milnikel, R.: Derivability in certain subsystems of the Logic of Proofs is $\\Pi^p_2$ -complete. Annals of Pure and Applied Logic\u00a0145(3), 223\u2013239 (2007)","journal-title":"Annals of Pure and Applied Logic"},{"key":"24_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1007\/3-540-63045-7_27","volume-title":"Logical Foundations of Computer Science","author":"A. Mkrtychev","year":"1997","unstructured":"Mkrtychev, A.: Models for the Logic of Proofs. In: Adian, S., Nerode, A. (eds.) LFCS 1997. LNCS, vol.\u00a01234, pp. 266\u2013275. Springer, Heidelberg (1997)"},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"Nour, K.: Classical combinatory logic. In: David, R., Gardy, D., Lescanne, P., Zaionc, M. (eds.) Computational Logic and Applications 2005. DMTCS proc. AF, pp. 87\u201396 (2006)","DOI":"10.46298\/dmtcs.3469"},{"key":"24_CR20","series-title":"Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/S0049-237X(08)70849-8","volume-title":"Proceedings of the 2nd Scandinavian Logic Symposium","author":"D. Prawitz","year":"1971","unstructured":"Prawitz, D.: Ideas and results in proof theory. In: Fenstad, J.E. (ed.) Proceedings of the 2nd Scandinavian Logic Symposium. Studies in Logic and the Foundations of Mathematics, vol.\u00a063, pp. 235\u2013307. North-Holland, Amsterdam (1971)"},{"key":"24_CR21","unstructured":"Renne, B.: Tableaux for the Logic of Proofs. Technical Report TR\u20132004001, CUNY Ph.D. Program in Computer Science (2004)"},{"key":"24_CR22","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-7643-7304-0_8","volume-title":"Logica Universalis","author":"L. Stra\u00dfburger","year":"2005","unstructured":"Stra\u00dfburger, L.: What is a logic, and what is a proof? In: Beziau, J.-Y. (ed.) Logica Universalis, pp. 135\u2013145. Birkh\u00e4user, Basel (2005)"},{"issue":"1","key":"24_CR23","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1023\/A:1020537107897","volume":"29","author":"R. Thiele","year":"2002","unstructured":"Thiele, R., Wos, L.: Hilbert\u2019s twenty-fourth problem. Journal of Automated Reasoning\u00a029(1), 67\u201389 (2002)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-72734-7_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,12]],"date-time":"2023-05-12T18:30:19Z","timestamp":1683916219000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-72734-7_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540727323","9783540727347"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-72734-7_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}