{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:18:11Z","timestamp":1725664691332},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540630456"},{"type":"electronic","value":"9783540690658"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63045-7_18","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:59:54Z","timestamp":1330279194000},"page":"167-177","source":"Crossref","is-referenced-by-count":13,"title":["Operational logic of proofs with functionality condition on proof predicate"],"prefix":"10.1007","author":[{"given":"Vladimir N.","family":"Krupski","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,25]]},"reference":[{"key":"18_CR1","unstructured":"S. Art\u00cbmov, Operational Modal Logic, Tech. Rep. 95-29, Mathematical Sciences Institute, Cornell University, December 1995."},{"key":"18_CR2","first-page":"39","volume":"4","author":"K. G\u00f6del","year":"1933","unstructured":"K. G\u00f6del, Eine Interpretation des intuitionistischen Aussagenkalk\u00fcls, Ergebnisse Math. Colloq., Bd. 4 (1933). S. 39\u201340.","journal-title":"Ergebnisse Math. Colloq."},{"key":"18_CR3","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF02757006","volume":"25","author":"R.M. Solovay","year":"1976","unstructured":"R.M. Solovay, Provability interpretations of modal logic, Israel J. Math., 25 (1976), pp. 287\u2013304.","journal-title":"Israel J. Math."},{"key":"18_CR4","volume-title":"Tech. Rep. IAM 92\u2013004","author":"S. Art\u00cbmov","year":"1993","unstructured":"S. Art\u00cbmov and T. Stra\\en, Functionality in the basic logic of proofs, Tech. Rep. IAM 92\u2013004, Department for Computer Science, University of Bern, Switzerland, Jan. 1993."},{"key":"18_CR5","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/0168-0072(94)90007-8","volume":"67","author":"S. Art\u00cbmov","year":"1994","unstructured":"S. Art\u00cbmov, Logic of proofs, Annals of Pure and Applied Logic, v. 67 (1994), pp. 29\u201359.","journal-title":"Annals of Pure and Applied Logic"},{"issue":"2","key":"18_CR6","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","volume":"16","author":"M.S. Paterson","year":"1978","unstructured":"M.S. Paterson and M.N. Wegman, Linear unification, J. Comput. System Sci., v.16 (2) (1978), pp. 158\u2013167.","journal-title":"J. Comput. System Sci."},{"key":"18_CR7","unstructured":"D. Hilbert and P. Bernays, Grundlagen der Mathematik, Springer, 1934\u20131939."},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"D. van Dalen, Logic and Structure, Springer-Verlag, 1994.","DOI":"10.1007\/978-3-662-02962-6"},{"key":"18_CR9","volume-title":"Theory of recursive functions and effective computability","author":"H. Rogers","year":"1967","unstructured":"H. Rogers, Theory of recursive functions and effective computability, McGraw-Hill Book Company, New York, 1967."},{"key":"18_CR10","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/3-540-58140-5_4","volume":"813","author":"S. Art\u00cbmov","year":"1994","unstructured":"S. Art\u00cbmov and V. Krupski, Referential data structures and labeled modal logic, Lecture Notes in Computer Science, v.813 (1994), pp. 23\u201333.","journal-title":"Lecture Notes in Computer Science"},{"key":"18_CR11","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0168-0072(95)00062-3","volume":"78","author":"S. Art\u00cbmov","year":"1996","unstructured":"S. Art\u00cbmov and V. Krupski, Data storage interpretation of labeled modal logic, Annals of Pure and Applied Logic, v.78 (1996), pp. 57\u201371.","journal-title":"Annals of Pure and Applied Logic"}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63045-7_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:41:15Z","timestamp":1619559675000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63045-7_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540630456","9783540690658"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-63045-7_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}