{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T10:40:02Z","timestamp":1749724802612,"version":"3.41.0"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2003,3,1]],"date-time":"2003-03-01T00:00:00Z","timestamp":1046476800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,3,1]],"date-time":"2003-03-01T00:00:00Z","timestamp":1046476800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Logic, Language and Information"],"published-print":{"date-parts":[[2003,3]]},"DOI":"10.1023\/a:1022363219134","type":"journal-article","created":{"date-parts":[[2003,3,28]],"date-time":"2003-03-28T22:25:21Z","timestamp":1048890321000},"page":"213-225","source":"Crossref","is-referenced-by-count":3,"title":["A Cut-Free Gentzen Formulation of Basic Propositional Calculus"],"prefix":"10.1007","volume":"12","author":[{"given":"Kentaro","family":"Kikuchi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Katsumi","family":"Sasaki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5098738_CR1","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1002\/(SICI)1521-3870(200005)46:2<199::AID-MALQ199>3.0.CO;2-B","volume":"46","author":"M. Aghaei","year":"2000","unstructured":"Aghaei, M. and Ardeshir, M., 2000, \u201cA bounded translation of intuitionistic propositional logic into basic propositional logic,\u201d Mathematical Logic Quarterly\n46, 199\u2013206.","journal-title":"Mathematical Logic Quarterly"},{"key":"5098738_CR2","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1023\/A:1012499207246","volume":"68","author":"a. Aghaei,M","year":"2001","unstructured":"Aghaei,M. and Ardeshir, M., 2001, \u201cGentzen-style axiomatizations for some conservative extensions of basic propositional logic,\u201d Studia Logica\n68, 263\u2013285.","journal-title":"Studia Logica"},{"key":"5098738_CR3","volume-title":"Aspects of basic logic","author":"M. Ardeshir","year":"1995","unstructured":"Ardeshir, M., 1995, \u201cAspects of basic logic,\u201d Ph.D. Thesis, Marquette University, Milwaukee."},{"key":"5098738_CR4","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1002\/malq.19980440304","volume":"44","author":"M. Ardeshir","year":"1998","unstructured":"Ardeshir, M. and Ruitenburg, W., 1998, \u201cBasic propositional calculus I,\u201d Mathematical Logic Quarterly\n44, 317\u2013343.","journal-title":"Mathematical Logic Quarterly"},{"key":"5098738_CR5","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/PL00003844","volume":"40","author":"M. Ardeshir","year":"2001","unstructured":"Ardeshir, M. and Ruitenburg, W., 2001, \u201cBasic propositional calculus II. Interpolation,\u201d Archive for Mathematical Logic\n40, 349\u2013364.","journal-title":"Archive for Mathematical Logic"},{"key":"5098738_CR6","volume-title":"Linear type theories, semantics and action calculi","author":"A. Barber","year":"1997","unstructured":"Barber, A., 1997, \u201cLinear type theories, semantics and action calculi,\u201d Ph.D. Thesis, LFCS, University of Edinburgh."},{"key":"5098738_CR7","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1023\/A:1005291931660","volume":"65","author":"G.M. Bierman","year":"2000","unstructured":"Bierman, G.M. and de Paiva, V.C.V., 2000, \u201cOn an intuitionistic modal logic,\u201d Studia Logica\n65, 383\u2013416.","journal-title":"Studia Logica"},{"key":"5098738_CR8","first-page":"258","volume-title":"Proceedings of the 23rd Annual Symposium on Principles of Programming Languages, St. Petersburg Beach, FL","author":"R. Davies","year":"1996","unstructured":"Davies, R. and Pfenning, F., 1996, \u201cA modal analysis of staged computation,\u201d pp. 258\u2013270 in Proceedings of the 23rd Annual Symposium on Principles of Programming Languages, St. Petersburg Beach, FL, G. Steele, Jr., ed., New York: ACM Press."},{"key":"5098738_CR9","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"Gentzen, G., 1935, \u201cUntersuchungen \u00fcber das logische Schliessen,\u201d Mathematische Zeitschrift\n39, 176\u2013210, 405\u2013431. English translation: pp. 68\u2013131 in The Collected Papers of Gerhard Gentzen, M.E. Szabo, ed., Amsterdam: North-Holland.","journal-title":"Mathematische Zeitschrift"},{"key":"5098738_CR10","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1016\/0168-0072(93)90093-S","volume":"59","author":"J.-Y. Girard","year":"1993","unstructured":"Girard, J.-Y., 1993, \u201cOn the unity of logic,\u201d Annals of Pure and Applied Logic\n59, 201\u2013217.","journal-title":"Annals of Pure and Applied Logic"},{"key":"5098738_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1007\/3-540-61208-4_14","volume-title":"Proceedings of Theorem Proving with Analytic Tableaux and Related Methods, 5th International Workshop, TABLEAUX\u2019 96, Terrasini, Palermo, Italy","author":"A. Heuerding","year":"1996","unstructured":"Heuerding, A., Seyfried, M., and Zimmermann, H., 1996, \u201cEfficient loop-check for backward proof search in some non-classical propositional logics,\u201d pp. 210\u2013225 in Proceedings of Theorem Proving with Analytic Tableaux and Related Methods, 5th International Workshop, TABLEAUX\u2019 96, Terrasini, Palermo, Italy, P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, eds., Lecture Notes in Artificial Intelligence, Vol. 1071, Berlin: Springer-Verlag."},{"key":"5098738_CR12","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1006\/inco.1994.1036","volume":"110","author":"J.S. Hodas","year":"1994","unstructured":"Hodas, J.S. and Miller, D., 1994, \u201cLogic programming in a fragment of intuitionistic linear logic,\u201d Information and Computation\n110, 327\u2013365.","journal-title":"Information and Computation"},{"key":"5098738_CR13","doi-asserted-by":"crossref","unstructured":"Ishii, K., Kashima, R., and Kikuchi, K., 2000, \u201cSequent calculi for Visser's propositional logics,\u201d Notre Dame Journal of Formal Logic, to appear.","DOI":"10.1305\/ndjfl\/1054301352"},{"key":"5098738_CR14","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1002\/1521-3870(200201)48:1<87::AID-MALQ87>3.0.CO;2-N","volume":"48","author":"K. Kikuchi","year":"2002","unstructured":"Kikuchi, K., 2002, \u201cDual-context sequent calculus and strict implication,\u201d Mathematical Logic Quarterly\n48, 87\u201392.","journal-title":"Mathematical Logic Quarterly"},{"key":"5098738_CR15","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/0168-0072(92)90029-Y","volume":"58","author":"A. Masini","year":"1992","unstructured":"Masini, A., 1992, \u201c2-Sequent calculus: A proof theory of modalities,\u201d Annals of Pure and Applied Logic\n58, 229\u2013246.","journal-title":"Annals of Pure and Applied Logic"},{"key":"5098738_CR16","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1023\/A:1005298819843","volume":"63","author":"W. Ruitenburg","year":"1999","unstructured":"Ruitenburg, W., 1999, \u201cBasic logic, K4, and persistence,\u201d Studia Logica\n63, 343\u2013352.","journal-title":"Studia Logica"},{"key":"5098738_CR17","first-page":"343","volume":"12","author":"K. Sasaki","year":"1998","unstructured":"Sasaki, K., 1998, \u201cA Gentzen-style formulation for Visser's propositional logic,\u201d Nanzan Management Review\n12, 343\u2013351.","journal-title":"Nanzan Management Review"},{"key":"5098738_CR18","first-page":"65","volume":"33","author":"K. Sasaki","year":"1999","unstructured":"Sasaki, K., 1999, \u201cFormalizations for the consequence relation of Visser's propositional logic,\u201d Reports on Mathematical Logic\n33, 65\u201378.","journal-title":"Reports on Mathematical Logic"},{"key":"5098738_CR19","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1023\/A:1008237600846","volume":"7","author":"Y. Suzuki","year":"1998","unstructured":"Suzuki, Y., Wolter, F., and Zakharyaschev, M., 1998, \u201cSpeaking about transitive frames in propositional languages,\u201d Journal of Logic, Language and Information\n7, 317\u2013339.","journal-title":"Journal of Logic, Language and Information"},{"key":"5098738_CR20","unstructured":"Szabo, M.E., ed., 1969, The Collected Papers of Gerhard Gentzen, Amsterdam: North-Holland."},{"key":"5098738_CR21","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/BF01874706","volume":"40","author":"A. Visser","year":"1981","unstructured":"Visser, A., 1981, \u201cA propositional logic with explicit fixed points,\u201d Studia Logica\n40, 155\u2013175.","journal-title":"Studia Logica"},{"key":"5098738_CR22","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/978-94-011-5638-7_8","volume-title":"Logic, Language and Computation","author":"H. Wansing","year":"1997","unstructured":"Wansing, H., 1997, \u201cDisplaying as temporalizing, sequent systems for subintuitionistic logics,\u201d pp. 159\u2013178 in Logic, Language and Computation, S. Akama, ed., Dordrecht: Kluwer Academic Publishers."}],"container-title":["Journal of Logic, Language and Information"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1022363219134.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1022363219134\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1022363219134.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T10:27:12Z","timestamp":1749724032000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1022363219134"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,3]]},"references-count":22,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,3]]}},"alternative-id":["5098738"],"URL":"https:\/\/doi.org\/10.1023\/a:1022363219134","relation":{},"ISSN":["0925-8531","1572-9583"],"issn-type":[{"type":"print","value":"0925-8531"},{"type":"electronic","value":"1572-9583"}],"subject":[],"published":{"date-parts":[[2003,3]]}}}