{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T23:00:52Z","timestamp":1762297252409,"version":"build-2065373602"},"reference-count":65,"publisher":"Elsevier","isbn-type":[{"type":"print","value":"9780444516909"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1016\/s1570-2464(07)80005-x","type":"book-chapter","created":{"date-parts":[[2007,10,4]],"date-time":"2007-10-04T09:38:50Z","timestamp":1191490730000},"page":"85-138","source":"Crossref","is-referenced-by-count":48,"title":["2 Modal proof theory"],"prefix":"10.1016","member":"78","reference":[{"key":"10.1016\/S1570-2464(07)80005-X_bib1","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/j.apal.2004.10.004","article-title":"About cut elimination for logics of common knowledge","volume":"133","author":"Alberucci","year":"2005","journal-title":"Annals of Pure and Applied Logic"},{"article-title":"Evidence-based common knowledge","year":"2004","author":"Artemov","key":"10.1016\/S1570-2464(07)80005-X_bib2"},{"key":"10.1016\/S1570-2464(07)80005-X_bib3","series-title":"Logic: Foundations to Applications","first-page":"1","article-title":"The method of hypersequents in the proof theory of propositional non-classical logics","author":"Avron","year":"1996"},{"key":"10.1016\/S1570-2464(07)80005-X_bib4","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/BF00284976","article-title":"Display logic","volume":"11","author":"Belnap","year":"1982","journal-title":"Journal of Philosophical Logic"},{"year":"1959","series-title":"The Foundations of Mathematics","author":"Beth","key":"10.1016\/S1570-2464(07)80005-X_bib5"},{"year":"2001","series-title":"Modal Logic","author":"Blackburn","key":"10.1016\/S1570-2464(07)80005-X_bib6"},{"key":"10.1016\/S1570-2464(07)80005-X_bib7","doi-asserted-by":"crossref","first-page":"763","DOI":"10.2977\/prims\/1195169271","article-title":"A perspective on modal sequent logic","volume":"27","author":"Blarney","year":"1991","journal-title":"Publications of the Research Institute for Mathematical Sciences, Kyoto University"},{"year":"1979","series-title":"The Unprovability of Consistency","author":"Boolos","key":"10.1016\/S1570-2464(07)80005-X_bib8"},{"year":"1993","series-title":"The Logic of Provability","author":"Boolos","key":"10.1016\/S1570-2464(07)80005-X_bib9"},{"key":"10.1016\/S1570-2464(07)80005-X_bib10","series-title":"Diamonds and Defauots","first-page":"67","article-title":"Interpreting modal natural deduction in type theory","author":"Borghuis","year":"1993"},{"year":"1998","series-title":"Handbook of Tableau Methods","key":"10.1016\/S1570-2464(07)80005-X_bib11"},{"key":"10.1016\/S1570-2464(07)80005-X_bib12","series-title":"Proc. Tableaux '99","first-page":"155","article-title":"Cut-free display calculi for nominal tense logics","author":"Demri","year":"1999"},{"key":"10.1016\/S1570-2464(07)80005-X_bib13","doi-asserted-by":"crossref","first-page":"149","DOI":"10.2307\/2273797","article-title":"Sequent systems for modal logic","volume":"50","author":"Do\u0161en","year":"1985","journal-title":"Journal of Symbolic Logic"},{"year":"1993","series-title":"Substructural Logics","key":"10.1016\/S1570-2464(07)80005-X_bib14"},{"year":"1995","series-title":"Reasoning About Knowledge","author":"Fagin","key":"10.1016\/S1570-2464(07)80005-X_bib15"},{"year":"1952","series-title":"Symbolic Logic, An Introduction","author":"Fitch","key":"10.1016\/S1570-2464(07)80005-X_bib16"},{"key":"10.1016\/S1570-2464(07)80005-X_bib17","first-page":"27","article-title":"Natural deduction rules for obligation","volume":"3","author":"Fitch","year":"1995","journal-title":"American Philosophical Quarterly"},{"key":"10.1016\/S1570-2464(07)80005-X_bib18","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1305\/ndjfl\/1093894722","article-title":"Tableau methods of proof for modal logics","volume":"13","author":"C. Fitting","year":"1972","journal-title":"Notre Dame Journal of Formal Logic"},{"year":"1983","series-title":"Proof Methods for Modal and Intuitionistic Logics","author":"C. Fitting","key":"10.1016\/S1570-2464(07)80005-X_bib19"},{"key":"10.1016\/S1570-2464(07)80005-X_bib20","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1093\/logcom\/1.1.83","article-title":"Destructive modal resolution","volume":"1","author":"C. Fitting","year":"1990","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/S1570-2464(07)80005-X_bib21","series-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","first-page":"368","article-title":"Basic modal logic","author":"C. Fitting","year":"1993"},{"year":"1996","series-title":"First-Order Logic and Automated Theorem Proving","author":"C. Fitting","key":"10.1016\/S1570-2464(07)80005-X_bib22"},{"key":"10.1016\/S1570-2464(07)80005-X_bib23","series-title":"A Companion to Philosophical Logic","first-page":"410","article-title":"First order alethic modal logic","author":"C. Fitting","year":"2002"},{"year":"2002","series-title":"Types, Tableaus, and G\u00f6del's God","author":"C. Fitting","key":"10.1016\/S1570-2464(07)80005-X_bib24"},{"key":"10.1016\/S1570-2464(07)80005-X_bib25","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1016\/j.apal.2003.11.014","article-title":"First-order intensional logic","volume":"127","author":"C. Fitting","year":"2004","journal-title":"Annals of Pure and Applied Logic"},{"year":"1998","series-title":"First-Order Modal Logic","author":"C. Fitting","key":"10.1016\/S1570-2464(07)80005-X_bib26"},{"year":"1996","series-title":"Labelled Deductive Systems","author":"M. Gabbay","key":"10.1016\/S1570-2464(07)80005-X_bib27"},{"key":"10.1016\/S1570-2464(07)80005-X_bib28","series-title":"Handbook of Philosophical Logic","first-page":"249","article-title":"Quantification in modal logic","author":"W. Garson","year":"1984"},{"key":"10.1016\/S1570-2464(07)80005-X_bib29_1","series-title":"The Collected Papers of Gerhard Gentzen","first-page":"68","article-title":"Investigation into logical deduction","author":"Gentzen","year":"1969"},{"key":"10.1016\/S1570-2464(07)80005-X_bib29_2","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","article-title":"Untersuchungen \u00fcber das logische Schliessen","volume":"39","year":"1935","journal-title":"Mathematische Zeitschrift"},{"key":"10.1016\/S1570-2464(07)80005-X_bib29_3","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/BF01201363","article-title":"Untersuchungen \u00fcber das logische Schliessen","volume":"39","year":"1935","journal-title":"Mathematische Zeitschrift"},{"key":"10.1016\/S1570-2464(07)80005-X_bib30","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1006\/inco.1999.2852","article-title":"Combining deduction and model checking into tableaux and algo- rithms for converse-PDL","volume":"162","author":"De Giacomo","year":"2000","journal-title":"Information and Computation"},{"key":"10.1016\/S1570-2464(07)80005-X_bib31_1","first-page":"300","article-title":"An interpretation of the intuitionistic propositional calculus","volume":"Volume One","author":"G\u00f6del","year":"1986"},{"key":"10.1016\/S1570-2464(07)80005-X_bib31_2","first-page":"39","article-title":"Eine Interpretation des intuitionistischen Aussagenkalk\u00fcls","volume":"vol 4","year":"1933","journal-title":"Ergebnisse eines mathematischen Kolloquiums"},{"year":"1987","series-title":"Logics of Time and Computation","author":"Goldblatt","key":"10.1016\/S1570-2464(07)80005-X_bib32"},{"year":"1998","series-title":"Tableau methods for modal and temporal logics","author":"Gor\u00e9","key":"10.1016\/S1570-2464(07)80005-X_bib33"},{"key":"10.1016\/S1570-2464(07)80005-X_bib34","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1016\/0004-3702(92)90049-4","article-title":"A guide to completeness and complexity for modal logics of knowledge and belief","volume":"54","author":"Halpern","year":"1992","journal-title":"Artificial Intelligence"},{"year":"2000","series-title":"Dynamic Logic","author":"Harel","key":"10.1016\/S1570-2464(07)80005-X_bib35"},{"year":"1962","series-title":"Knowledge and Belief","author":"Hintikka","key":"10.1016\/S1570-2464(07)80005-X_bib36"},{"year":"1996","series-title":"A New Introduction to Modal Logic","author":"Hughes","key":"10.1016\/S1570-2464(07)80005-X_bib37"},{"key":"10.1016\/S1570-2464(07)80005-X_bib38","first-page":"15","article-title":"Generalized sequent calculus for propositional modal logics","volume":"1","author":"Indrzejczak","year":"1997","journal-title":"Logica Trianguli"},{"key":"10.1016\/S1570-2464(07)80005-X_bib39","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1093\/jigpal\/6.3.505","article-title":"Cut-free double sequent calculus for S5","volume":"6","author":"Indrzejczak","year":"1998","journal-title":"Logic Journal of the IGPL"},{"key":"10.1016\/S1570-2464(07)80005-X_bib40","first-page":"1","article-title":"On the rules of suppositions in formal logic","author":"J\u00e0skowski","year":"1934","journal-title":"Studia Logica"},{"key":"10.1016\/S1570-2464(07)80005-X_bib41","series-title":"Proceedings of the Ninth International Colloquium on Automata, Languages, and Programming","first-page":"348","article-title":"Results on the propositional \u03bc-calculus","volume":"140","author":"Kozen","year":"1982"},{"key":"10.1016\/S1570-2464(07)80005-X_bib42","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1137\/0206033","article-title":"The computational complexity of provability in systems of modal propositional logic","volume":"6","author":"E. Ladner","year":"1977","journal-title":"SIAM J. Comput."},{"year":"1997","series-title":"The Resolution Calculus","author":"Leitsch","key":"10.1016\/S1570-2464(07)80005-X_bib43"},{"key":"10.1016\/S1570-2464(07)80005-X_bib44","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/BF02120399","article-title":"Wynikanie semantyczne a wynikanie formalne (logical consequence, semantic and formal)","volume":"10","author":"Lis","year":"1960","journal-title":"Studia Logica"},{"key":"10.1016\/S1570-2464(07)80005-X_bib45","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/0168-0072(92)90029-Y","article-title":"2-sequent calculus: a proof theory of modalities","volume":"58","author":"Masini","year":"1992","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/S1570-2464(07)80005-X_bib46","series-title":"Proceedings of CADE 12, volume 814 of Lecture Notes in Artificial Intelligence","first-page":"723","article-title":"Strongly analytic tableaux for normal modal logics","author":"Massacci","year":"1994"},{"key":"10.1016\/S1570-2464(07)80005-X_bib47","first-page":"113","article-title":"Gentzen method in modal calculi I","volume":"9","author":"Ohnishi","year":"1957","journal-title":"Osaka Mathematical Journal"},{"key":"10.1016\/S1570-2464(07)80005-X_bib48","first-page":"115","article-title":"Gentzen method in modal calculi II","volume":"11","author":"Ohnishi","year":"1959","journal-title":"Osaka Mathematical Journal"},{"key":"10.1016\/S1570-2464(07)80005-X_bib49","series-title":"Proof Theory of Modal Logic","first-page":"55","article-title":"Relational proof systems for modal logics","author":"Orlowska","year":"1996"},{"year":"2002","series-title":"Substructural Logics: A Primer","author":"Paoli","key":"10.1016\/S1570-2464(07)80005-X_bib50"},{"key":"10.1016\/S1570-2464(07)80005-X_bib51","series-title":"Proceedings of the Tenth Symposium on the Theory of Computation","first-page":"326","article-title":"A practical decision method for propositional dynamic logic","author":"Pratt","year":"1978"},{"key":"10.1016\/S1570-2464(07)80005-X_bib52","article-title":"Natural Deduction, A Proof-Theoretical Study","volume":"3","author":"Prawitz","year":"1965"},{"year":"2000","series-title":"An Introduction to Substructural Logics","author":"Restall","key":"10.1016\/S1570-2464(07)80005-X_bib53"},{"key":"10.1016\/S1570-2464(07)80005-X_bib54","series-title":"Proceedings of the Third Scandinavian Logic Symposium, Uppsala 1973","first-page":"110","article-title":"Completeness and correspondence in the first and second order semantics for modal logic","author":"Sahlqvist","year":"1975"},{"key":"10.1016\/S1570-2464(07)80005-X_bib55","doi-asserted-by":"crossref","first-page":"631","DOI":"10.1305\/ndjfl\/1093888133","article-title":"Fitch-style rules for many modal logics","volume":"18","author":"Siemens","year":"1977","journal-title":"Notre Dame Journal of Formal Logic"},{"year":"1985","series-title":"Self-reference and Modal Logic","author":"Smory\u0144ski","key":"10.1016\/S1570-2464(07)80005-X_bib56"},{"year":"1968","series-title":"First-Order Logic","author":"M. Smullyan","key":"10.1016\/S1570-2464(07)80005-X_bib57"},{"key":"10.1016\/S1570-2464(07)80005-X_bib58","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1093\/logcom\/4.2.125","article-title":"Sequent systems for normal modal propositional logics","volume":"4","author":"Wansing","year":"1994","journal-title":"Journal of Logic and Compu- tation"},{"year":"1996","series-title":"Proof Theory of Modal Logic","key":"10.1016\/S1570-2464(07)80005-X_bib59"},{"year":"1998","series-title":"Displaying Modal Logic","author":"Wansing","key":"10.1016\/S1570-2464(07)80005-X_bib60"},{"key":"10.1016\/S1570-2464(07)80005-X_bib61","doi-asserted-by":"crossref","first-page":"719","DOI":"10.1093\/jigpal\/6.5.719","article-title":"Translation of hypersequents into display sequents","volume":"6","author":"Wansing","year":"1998","journal-title":"Journal of the IGPL"},{"key":"10.1016\/S1570-2464(07)80005-X_bib62","series-title":"Handbook of Philosophical Logic","first-page":"61","article-title":"Sequent systems for modal logics","author":"Wansing","year":"2002"}],"container-title":["Studies in Logic and Practical Reasoning","Handbook of Modal Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157024640780005X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S157024640780005X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T23:13:25Z","timestamp":1761606805000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S157024640780005X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9780444516909"],"references-count":65,"URL":"https:\/\/doi.org\/10.1016\/s1570-2464(07)80005-x","relation":{},"ISSN":["1570-2464"],"issn-type":[{"type":"print","value":"1570-2464"}],"subject":[],"published":{"date-parts":[[2007]]}}}