{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,3]],"date-time":"2025-12-03T18:05:49Z","timestamp":1764785149761,"version":"3.37.3"},"reference-count":71,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2023,6,14]],"date-time":"2023-06-14T00:00:00Z","timestamp":1686700800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,6,14]],"date-time":"2023-06-14T00:00:00Z","timestamp":1686700800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[2023,12]]},"DOI":"10.1007\/s11225-023-10052-7","type":"journal-article","created":{"date-parts":[[2023,6,14]],"date-time":"2023-06-14T09:02:19Z","timestamp":1686733339000},"page":"979-1014","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Refutation-Aware Gentzen-Style Calculi for Propositional Until-Free Linear-Time Temporal Logic"],"prefix":"10.1007","volume":"111","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7736-8055","authenticated-orcid":false,"given":"Norihiro","family":"Kamide","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,6,14]]},"reference":[{"issue":"2","key":"10052_CR1","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/77600.77617","volume":"37","author":"M Abadi","year":"1990","unstructured":"Abadi, M., and Z. Manna, Nonclausal deduction in first-order temporal logic, Journal of the ACM 37 (2): 279\u2013317, 1990.","journal-title":"Journal of the ACM"},{"issue":"1","key":"10052_CR2","doi-asserted-by":"publisher","first-page":"231","DOI":"10.2307\/2274105","volume":"49","author":"A Almukdad","year":"1984","unstructured":"Almukdad, A., and D. Nelson, Constructible falsity and inexact predicates, Journal of Symbolic Logic 49 (1): 231\u2013233, 1984.","journal-title":"Journal of Symbolic Logic"},{"issue":"8","key":"10052_CR3","doi-asserted-by":"publisher","first-page":"965","DOI":"10.1007\/s00153-004-0237-z","volume":"43","author":"S Baratella","year":"2004","unstructured":"Baratella, S., and A. Masini, An approach to infinitary temporal proof theory, Archive for Mathematical Logic 43 (8): 965\u2013990, 2004.","journal-title":"Archive for Mathematical Logic"},{"key":"10052_CR4","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-94-010-1161-7_2","volume-title":"Modern Uses of Multiple-Valued Logic","author":"ND Belnap","year":"1977","unstructured":"Belnap, N. D., A useful four-valued logic, in: G. Epstein, and J. M. Dunn, (eds.), Modern Uses of Multiple-Valued Logic, Dordrecht, Reidel, 1977, pp. 5\u201337."},{"key":"10052_CR5","first-page":"30","volume-title":"Contemporary Aspects of Philosophy","author":"ND Belnap","year":"1977","unstructured":"Belnap, N. D., How a computer should think, in: G. Ryle, (ed.), Contemporary Aspects of Philosophy, Oriel Press, Stocksfield, 1977, pp. 30\u201356."},{"issue":"2","key":"10052_CR6","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1016\/j.jlap.2008.02.004","volume":"76","author":"K Br\u00fcnnler","year":"2008","unstructured":"Br\u00fcnnler, K., and M. Lange, Cut-free sequent systems for temporal logic, Journal of Logic and Algebraic Methods in Programming 76 (2): 216\u2013225, 2008.","journal-title":"Journal of Logic and Algebraic Methods in Programming"},{"key":"10052_CR7","doi-asserted-by":"crossref","unstructured":"Cavalli, A. R., and L. Fari\u00f1as del Cerro, A Decision Method for Linear Temporal Logic, vol. 170 of Lecture Notes in Computer Science, 1984, pp. 113\u2013127.","DOI":"10.1007\/978-0-387-34768-4_7"},{"key":"10052_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., and E. A. Emerson, Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic, vol. 131 of Lecture Notes in Computer Science, 1981, pp. 52\u201371.","DOI":"10.1007\/BFb0025774"},{"issue":"5","key":"10052_CR9","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke, E. M., O. Grumberg, S. Jha, Y. Lu, and H. Veith, Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM 50 (5): 752\u2013794, 2003.","journal-title":"Journal of the ACM"},{"key":"10052_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., T. A. Henzinger, H. Veith, and R. Bloem, (eds.), Handbook of Model Checking, Springer, 2018.","DOI":"10.1007\/978-3-319-10575-8"},{"key":"10052_CR11","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1305\/ndjfl\/1093888021","volume":"18","author":"J Czermak","year":"1977","unstructured":"Czermak, J., A remark on Gentzen\u2019s calculus of sequents, Notre Dame Journal of Formal Logic 18: 471\u2013474, 1977.","journal-title":"Notre Dame Journal of Formal Logic"},{"issue":"1","key":"10052_CR12","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1145\/1119439.1119443","volume":"7","author":"A Degtyarev","year":"2006","unstructured":"Degtyarev, A., M. Fisher, and B. Konev, Monodic temporal resolution, ACM Transaction on Computational Logic 7 (1): 108\u2013150, 2006.","journal-title":"ACM Transaction on Computational Logic"},{"key":"10052_CR13","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1023\/A:1018942108420","volume":"22","author":"C Dixon","year":"1998","unstructured":"Dixon, C., Temporal resolution using a breadth-first search algorithm, Annals of Mathematics and Artificial Intelligence 22: 87\u2013115, 1998.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"issue":"3","key":"10052_CR14","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF00373152","volume":"29","author":"JM Dunn","year":"1976","unstructured":"Dunn, J. M., Intuitive semantics for first-degree entailment and \u2018coupled trees\u2019, Philosophical Studies 29 (3): 149\u2013168, 1976.","journal-title":"Philosophical Studies"},{"key":"10052_CR15","doi-asserted-by":"crossref","unstructured":"Emerson, E. A., Temporal and modal logic, in: J. van Leeuwen, (ed.), Handbook of Theoretical Computer Science, Formal Models and Semantics (B), Elsevier and MIT Press, 1990, pp. 995\u20131072.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"10052_CR16","unstructured":"Fisher, M., A resolution method for temporal logic, in Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI), 1991, pp. 99\u2013104."},{"issue":"1","key":"10052_CR17","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/371282.371311","volume":"2","author":"M Fisher","year":"2001","unstructured":"Fisher, M., C. Dixon, and M. Peim, Clausal temporal resolution, ACM Transactions on Computational Logic 2 (1): 12\u201356, 2001.","journal-title":"ACM Transactions on Computational Logic"},{"key":"10052_CR18","doi-asserted-by":"crossref","unstructured":"Gaintzarain, J., M. Hermo, P. Lucio, M. Navarro, and F. Orejas, A cut-free and invariant-free sequent calculus for PLTL, in Proceedings of the 21st International Workshop on Computer Science Logic, Lecture Notes in Computer Science 4646, 2008, pp. 481\u2013495.","DOI":"10.1007\/978-3-540-74915-8_36"},{"key":"10052_CR19","unstructured":"Gentzen, G., The Collected Papers of Gerhard Gentzen, (english translation), M.E. Szabo, (ed.), vol. 55 of Studies in Logic and the Foundations of Mathematics, North-Holland, 1969."},{"key":"10052_CR20","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1002\/malq.19810270803","volume":"27","author":"ND Goodman","year":"1981","unstructured":"Goodman, N. D., The logic of contradiction, Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik 27: 119\u2013126, 1981.","journal-title":"Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik"},{"key":"10052_CR21","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/BF01054714","volume":"53","author":"V Goranko","year":"1994","unstructured":"Goranko, V., Refutation systems in modal logic, Studia Logica 53: 299\u2013324, 1994.","journal-title":"Studia Logica"},{"key":"10052_CR22","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., and M. Chechik, Why waste a perfectly good abstraction? in Proceedings of the 12th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 2006), vol. 3920 of Lecture Notes in Computer Science, 2006, pp. 212\u2013226.","DOI":"10.1007\/11691372_14"},{"key":"10052_CR23","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., O. Wei, and M. Chechik, Yasm: A software model-checker for verification and refutation, in Proceedings of the 18th International Conference on Computer Aided Verification (CAV 2006), 2006, pp. 170\u2013174.","DOI":"10.1007\/11817963_18"},{"key":"10052_CR24","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S0168-0072(00)00018-X","volume":"106","author":"I Hodkinson","year":"2000","unstructured":"Hodkinson, I., F. Wolter, and M. Zakharyaschev, Decidable fragments of first-order temporal logics, Annals of Pure and Applied Logic 106: 85\u2013134, 2000.","journal-title":"Annals of Pure and Applied Logic"},{"key":"10052_CR25","unstructured":"Horn, L. R., and H. Wansing, Negation, in Edward N. Zalta (ed.), The Stanford Encyclopedia of Philosophy (Spring 2017 Edition), Last modified on January 2017, https:\/\/plato.stanford.edu\/archives\/spr2017\/entries\/negation\/."},{"key":"10052_CR26","doi-asserted-by":"crossref","unstructured":"Hustadt, U., and B. Konev, TRP++2.0: A Temporal Resolution Prover, vol. 2741 of Lecture Notes in Artificial Intelligence, 2003, pp. 274\u2013278.","DOI":"10.1007\/978-3-540-45085-6_21"},{"issue":"4","key":"10052_CR27","doi-asserted-by":"publisher","first-page":"405","DOI":"10.3166\/jancl.15.405-435","volume":"15","author":"N Kamide","year":"2005","unstructured":"Kamide, N., Natural deduction systems for Nelson\u2019s paraconsistent logic and its neighbors, Journal of Applied Non-Classical Logics 15 (4): 405\u2013435, 2005.","journal-title":"Journal of Applied Non-Classical Logics"},{"issue":"4","key":"10052_CR28","first-page":"187","volume":"35","author":"N Kamide","year":"2006","unstructured":"Kamide, N., An equivalence between sequent calculi for linear-time temporal logic, Bulletin of the Section of the Logic 35 (4): 187\u2013194, 2006.","journal-title":"Bulletin of the Section of the Logic"},{"key":"10052_CR29","first-page":"1","volume":"2007","author":"N Kamide","year":"2007","unstructured":"Kamide, N., A uniform proof-theoretic foundation for abstract paraconsistent logic programming, Journal of Functional and Logic Programming, 1\u201336, 2007.","journal-title":"Journal of Functional and Logic Programming"},{"key":"10052_CR30","doi-asserted-by":"crossref","unstructured":"Kamide, N., Embedding linear-time temporal logic into infinitary logic: application to cut-elimination for multi-agent infinitary epistemic linear-time temporal logic, in Proceedings of the 9th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA9), vol. 5405 of Lecture Notes in Artificial Intelligence, 2009, pp. 57\u201376.","DOI":"10.1007\/978-3-642-02734-5_5"},{"key":"10052_CR31","doi-asserted-by":"crossref","unstructured":"Kamide, N., Reasoning about bounded time domain: An alternative to NP-complete fragments of LTL, in Proceedings of the 2nd International Conference on Agents and Artificial Intelligence (ICAART 2010), 2010, pp. 536\u2013539.","DOI":"10.5220\/0002714805360539"},{"issue":"4","key":"10052_CR32","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1016\/j.apal.2011.12.002","volume":"163","author":"N Kamide","year":"2012","unstructured":"Kamide, N., Bounded linear-time temporal logic: A proof-theoretic investigation, Annals of Pure and Applied Logic 163 (4): 439\u2013466, 2012.","journal-title":"Annals of Pure and Applied Logic"},{"issue":"1","key":"10052_CR33","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1017\/S0960129514000048","volume":"25","author":"N Kamide","year":"2015","unstructured":"Kamide, N., Embedding theorems for LTL and its variants, Mathematical Structures in Computer Science 25 (1): 83\u2013134, 2015.","journal-title":"Mathematical Structures in Computer Science"},{"issue":"7","key":"10052_CR34","doi-asserted-by":"publisher","first-page":"2271","DOI":"10.1093\/logcom\/exx006","volume":"27","author":"N Kamide","year":"2017","unstructured":"Kamide, N., Relating first-order monadic omega-logic, propositional linear-time temporal logic, propositional generalized definitional reflection logic and propositional infinitary logic, Journal of Logic and Computation 27 (7): 2271\u20132301, 2017.","journal-title":"Journal of Logic and Computation"},{"issue":"1","key":"10052_CR35","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/s10992-021-09611-x","volume":"51","author":"N Kamide","year":"2022","unstructured":"Kamide, N., Falsification-aware semantics and sequent calculi for classical logic, Journal of Philosophical Logic 51 (1): 99\u2013126, 2022.","journal-title":"Journal of Philosophical Logic"},{"issue":"1","key":"10052_CR36","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1142\/S0218194022500061","volume":"32","author":"N Kamide","year":"2022","unstructured":"Kamide, N., Inconsistency-tolerant hierarchical probabilistic CTL model checking: logical foundations and illustrative examples, International Journal of Software Engineering and Knowledge Engineering 32 (1): 131\u2013162, 2022.","journal-title":"International Journal of Software Engineering and Knowledge Engineering"},{"issue":"7","key":"10052_CR37","doi-asserted-by":"publisher","first-page":"971","DOI":"10.1142\/S0218194022500371","volume":"32","author":"N Kamide","year":"2022","unstructured":"Kamide, N., Falsification-aware semantics for temporal logics and their inconsistency-tolerant subsystems: Theoretical foundations of falsification-aware model checking, International Journal of Software Engineering and Knowledge Engineering 32 (7): 971\u20131017, 2022.","journal-title":"International Journal of Software Engineering and Knowledge Engineering"},{"key":"10052_CR38","doi-asserted-by":"crossref","unstructured":"Kamide, N., and S. Kanbe, Falsification-aware semantics for CTL and its inconsistency-tolerant subsystem: Towards falsification-aware model checking, in Proceedings of the 14th International Conference on Agents and Artificial Intelligence (ICAART 2022), vol. 3, 2022, pp. 242\u2013252.","DOI":"10.5220\/0010803700003116"},{"issue":"1","key":"10052_CR39","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3233\/FI-2011-374","volume":"106","author":"N Kamide","year":"2011","unstructured":"Kamide, N., and H. Wansing, A paraconsistent linear-time temporal logic, Fundamenta Informaticae 106 (1): 1\u201323, 2011.","journal-title":"Fundamenta Informaticae"},{"key":"10052_CR40","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2011.11.001","volume":"415","author":"N Kamide","year":"2012","unstructured":"Kamide, N., and H. Wansing, Proof theory of Nelson\u2019s paraconsistent logic: A uniform perspective, Theoretical Computer Science 415: 1\u201338, 2012","journal-title":"Theoretical Computer Science"},{"key":"10052_CR41","unstructured":"Kamide, N., and H. Wansing, Proof theory of N4-Related Paraconsistent Logics, vol. 54 of Studies in Logic, College Publications, 2015, pp. 1\u2013401."},{"issue":"4","key":"10052_CR42","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/s00354-009-0116-6","volume":"29","author":"K Kaneiwa","year":"2011","unstructured":"Kaneiwa, K., and N. Kamide, Paraconsistent computation tree logic, New Generation Computing 29 (4): 391\u2013408, 2011.","journal-title":"New Generation Computing"},{"key":"10052_CR43","doi-asserted-by":"crossref","unstructured":"Kapsner, A., Logics and Falsifications: A New Perspective on Constructivist Semantics, vol. 40 of Trends in Logic Book, Springer, 2014.","DOI":"10.1007\/978-3-319-05206-9"},{"key":"10052_CR44","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1002\/malq.19870330506","volume":"33","author":"H Kawai","year":"1987","unstructured":"Kawai, H., Sequential calculus for a first order infinitary temporal logic, Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik 33: 423\u2013432, 1987.","journal-title":"Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik"},{"issue":"1","key":"10052_CR45","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1093\/jigpal\/8.1.55","volume":"8","author":"O Lichtenstein","year":"2000","unstructured":"Lichtenstein, O., and A. Pnueli, Propositional temporal logics: decidability and completeness, Logic Journal of the IGPL 8 (1): 55\u201385, 2000.","journal-title":"Logic Journal of the IGPL"},{"key":"10052_CR46","unstructured":"\u0141ukasiewicz, J., Aristotle\u2019s Syllogistic from the Standpoint of Modern Formal Logic, Oxford, 1951 (Aristotle\u2019s Syllogistic from the Standpoint of Modern Formal Logic - Greek & Roman philosophy, Taylor & Francis, 1987)."},{"key":"10052_CR47","doi-asserted-by":"publisher","first-page":"59","DOI":"10.12775\/LLP.2002.004","volume":"10","author":"P \u0141ukowski","year":"2002","unstructured":"\u0141ukowski, P., A deductive-reductive form of logic: General theory and intuitionistic case, Logic and Logical Philosophy 10: 59\u201378, 2002.","journal-title":"Logic and Logical Philosophy"},{"key":"10052_CR48","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D Miller","year":"1991","unstructured":"Miller, D., G. Nadathur, F. Pfenning, and A. Scedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic 51: 125\u2013157, 1991.","journal-title":"Annals of Pure and Applied Logic"},{"key":"10052_CR49","doi-asserted-by":"publisher","first-page":"16","DOI":"10.2307\/2268973","volume":"14","author":"D Nelson","year":"1949","unstructured":"Nelson, D., Constructible falsity, Journal of Symbolic Logic 14: 16\u201326, 1949.","journal-title":"Journal of Symbolic Logic"},{"key":"10052_CR50","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/BFb0026305","volume":"385","author":"B Paech","year":"1988","unstructured":"Paech, B., Gentzen-Systems for Propositional Temporal Logics, vol. 385 of Lecture Notes in Computer Science, 1988, pp. 240\u2013253.","journal-title":"Lecture Notes in Computer Science"},{"key":"10052_CR51","doi-asserted-by":"crossref","unstructured":"Pliu\u0161kevi\u010dius, R., Investigation of Finitary Calculus for a Discrete Linear Time Logic by Means of Infinitary Calculus, vol. 502 of Lecture Notes in Computer Science, 1991, pp. 504\u2013528.","DOI":"10.1007\/BFb0019366"},{"key":"10052_CR52","doi-asserted-by":"crossref","unstructured":"Pnueli, A., The temporal logic of programs, in Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, 1977, pp. 46\u201357.","DOI":"10.1109\/SFCS.1977.32"},{"key":"10052_CR53","unstructured":"Priest, G., and K. Tanaka, Paraconsistent logic, in: E. N. Zalta (ed.), The Stanford Encyclopedia of Philosophy (Summer 2009 Edition), http:\/\/plato.stanford.edu\/archives\/sum2009\/entries\/logic-paraconsistent\/"},{"key":"10052_CR54","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/BF02120864","volume":"33","author":"C Rauszer","year":"1974","unstructured":"Rauszer, C., A formalization of the propositional calculus of H-B logic, Studia Logica 33: 23\u201334, 1974.","journal-title":"Studia Logica"},{"key":"10052_CR55","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/BF02121115","volume":"36","author":"C Rauszer","year":"1977","unstructured":"Rauszer, C., Applications of Kripke models to Heyting-Brouwer logic, Studia Logica 36: 61\u201371, 1977.","journal-title":"Studia Logica"},{"key":"10052_CR56","unstructured":"Rauszer, C., An Algebraic and Kripke-Style Approach to a Certain Extension of Intuitionistic Logic, Dissertations Mathematicae, Polish Scientific Publishers, 1980, pp. 1\u201367."},{"issue":"1","key":"10052_CR57","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J. A., A machine-oriented logic based on the resolution principle, Journal of the ACM, 12 (1): 23\u201341, 1965.","journal-title":"Journal of the ACM"},{"issue":"3","key":"10052_CR58","first-page":"199","volume":"4","author":"T Sakuragawa","year":"1987","unstructured":"Sakuragawa, T., Temporal Prolog: a programming language based on temporal logic, Computer Software 4 (3): 199\u2013211, 1987.","journal-title":"Computer Software"},{"issue":"2\u20133","key":"10052_CR59","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/s11225-005-8474-7","volume":"80","author":"Y Shramko","year":"2005","unstructured":"Shramko, Y., Dual intuitionistic logic and a variety of negations: The logic of scientific research, Studia Logica 80 (2\u20133): 347\u2013367, 2005.","journal-title":"Studia Logica"},{"issue":"2","key":"10052_CR60","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1017\/S1755020316000022","volume":"9","author":"Y Shramko","year":"2016","unstructured":"Shramko, Y., A modal translation for dual-intuitionistic logic, Review of Symbolic Logic 9 (2): 251\u2013265, 2016.","journal-title":"Review of Symbolic Logic"},{"key":"10052_CR61","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/BF01306967","volume":"24","author":"TF Skura","year":"1995","unstructured":"Skura, T. F., A \u0141ukasiewicz-style refutation system for the modal logic S4, Journal of Philosophical Logic 24: 573\u2013582, 1995.","journal-title":"Journal of Philosophical Logic"},{"issue":"2","key":"10052_CR62","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1023\/A:1015174332202","volume":"70","author":"TF Skura","year":"2002","unstructured":"Skura, T. F., Refutations, proofs, and models in the modal logic K4, Studia Logica 70 (2): 193\u2013204, 2002.","journal-title":"Studia Logica"},{"key":"10052_CR63","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-94-007-0479-4_2","volume":"16","author":"TF Skura","year":"2011","unstructured":"Skura, T. F., Refutation systems in propositional logic, Handbook of Philosophical Logic 16: 115\u2013157, 2011.","journal-title":"Handbook of Philosophical Logic"},{"key":"10052_CR64","doi-asserted-by":"publisher","first-page":"83","DOI":"10.4467\/20842589RM.17.005.7143","volume":"52","author":"TF Skura","year":"2017","unstructured":"Skura, T. F., Refutations in Wansing\u2019s logic, Reports on Mathematical Logic 52: 83\u201399, 2017.","journal-title":"Reports on Mathematical Logic"},{"key":"10052_CR65","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/3-540-11981-7_21","volume":"148","author":"ME Szabo","year":"1980","unstructured":"Szabo, M. E., A sequent calculus for Kr\u00f6ger logic, in A. Salwicki, (ed.), Logics of Programs and Their Applications, Proceedings, Poznan, August 23-29, 1980, vol. 148 of Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, 1980, pp. 295\u2013303.","journal-title":"Lecture Notes in Computer Science"},{"issue":"3","key":"10052_CR66","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/0304-3975(86)90157-X","volume":"47","author":"A Sza\u0142as","year":"1986","unstructured":"Sza\u0142as, A. Concerning the semantic consequence relation in first-order temporal logic, Theoretical Computer Science 47 (3): 329\u2013334, 1986.","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"10052_CR67","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1305\/ndjfl\/1039886520","volume":"37","author":"I Urbas","year":"1996","unstructured":"Urbas, I., Dual-intuitionistic logic, Notre Dame Journal of Formal Logic 37 (3): 440\u2013451, 1996.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"10052_CR68","unstructured":"Venkatesh, G., A Decision Method for Temporal Logic Based on Resolution, in S. N. Maheshwari, (ed.), Foundations of Software Technology and Theoretical Computer Science Fifth Conference, New Delhi, India, December 16-18, 1985, Proceedings, vol. 206 of Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, 1986, pp. 272\u2013289."},{"key":"10052_CR69","doi-asserted-by":"crossref","unstructured":"Wansing, H., The Logic of Information Structures, vol. 681 of Lecture Notes in Artificial Intelligence, Springer, Berlin, Heidelberg, 1993.","DOI":"10.1007\/3-540-56734-8"},{"key":"10052_CR70","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1305\/ndjfl\/1040308828","volume":"36","author":"H Wansing","year":"1995","unstructured":"Wansing, H., Semantics-based nonmonotonic inference, Notre Dame Journal of Formal Logic 36: 44\u201354, 1995.","journal-title":"Notre Dame Journal of Formal Logic"},{"issue":"1","key":"10052_CR71","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1093\/logcom\/ext035","volume":"26","author":"H Wansing","year":"2016","unstructured":"Wansing, H., Falsification, natural deduction and bi-intuitionistic logic, Journal of Logic and Computation 26 (1): 425\u2013450, 2016.","journal-title":"Journal of Logic and Computation"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-023-10052-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11225-023-10052-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-023-10052-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T07:30:09Z","timestamp":1729582209000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11225-023-10052-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,14]]},"references-count":71,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2023,12]]}},"alternative-id":["10052"],"URL":"https:\/\/doi.org\/10.1007\/s11225-023-10052-7","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[2023,6,14]]},"assertion":[{"value":"26 September 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 June 2023","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The author has no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}