{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:02Z","timestamp":1749125162233},"reference-count":89,"publisher":"Elsevier","isbn-type":[{"value":"9780444508133","type":"print"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1016\/b978-044450813-3\/50024-2","type":"book-chapter","created":{"date-parts":[[2007,6,11]],"date-time":"2007-06-11T13:04:11Z","timestamp":1181567051000},"page":"1487-1578","source":"Crossref","is-referenced-by-count":16,"title":["Connections in Nonclassical Logics"],"prefix":"10.1016","author":[{"given":"Arild","family":"Waaler","sequence":"first","affiliation":[]}],"member":"78","reference":[{"issue":"2","key":"10.1016\/B978-044450813-3\/50024-2_bb0010","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","article-title":"Theorem proving via general matings","volume":"28","author":"Andrews","year":"1981","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0015","series-title":"Advances in Modal Logic","first-page":"1","article-title":"Shakesperian modal logic","author":"Artosi","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0020","series-title":"Proceedings of the CADE-12 Workshop on Automated Model Building","first-page":"11","article-title":"Labelled model modal logic","author":"Artosi","year":"1994"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50024-2_bb0025","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1093\/logcom\/2.3.247","article-title":"Modal theorem proving: An equational viewpoint","volume":"2","author":"Auffray","year":"1992","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0030","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/BF01531058","article-title":"Using hypersequents in proof systems for non-classical logics","volume":"4","author":"Avron","year":"1991","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0035","first-page":"445","article-title":"Unification theory","volume":"Vol. I","author":"Baader","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0040","series-title":"Proc. 4th. Workshop on Deduction with Tableaux and Related Methods","first-page":"217","article-title":"Nonelementary speedups between different versions of tableaux","author":"Baaz","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0045","series-title":"International Conference on Theorem Proving with Analythic Tableaux and Related Methods","first-page":"91","article-title":"Free variable tableaux for propositional modal logics","author":"Beckert","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0050","series-title":"Proceedings, 11th. International Conference on Automated Deduction","first-page":"507","article-title":"An improved method for adding equality to free variable semantic tableaux","author":"Beckert","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0055","series-title":"Proceedings of the third Kurt G\u00f6del Colloquium","first-page":"108","article-title":"The even more liberalized d-rule in free variable semantic tableaux","author":"Beckert","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0060","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"},{"issue":"4","key":"10.1016\/B978-044450813-3\/50024-2_bb0065","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1145\/322276.322277","article-title":"On matrices with connections","volume":"28","author":"Bibel","year":"1981","journal-title":"Journal of the ACM"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0070","series-title":"Automated Theorem Proving","author":"Bibel","year":"1982"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50024-2_bb0075","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0004-3702(82)90024-8","article-title":"A comparative study of several proof procedures","volume":"18","author":"Bibel","year":"1982","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0080","series-title":"Proceedings of the Herbrand Symposium, Logic Colloquium '81","first-page":"11","article-title":"Computationally improved versions of Herbrand's Theorem","author":"Bibel","year":"1982"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0085","series-title":"Automated Theorem Proving","author":"Bibel","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0090","first-page":"68","article-title":"Methods and calculi for deduction","volume":"Vol. 1","author":"Bibel","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0095","series-title":"Machine Intelligence","first-page":"101","article-title":"The sharing of structure in theorem-proving programs","author":"Boyer","year":"1972"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0100","first-page":"1","article-title":"Basic modal logic","volume":"Vol. 2","author":"Bull","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0105","doi-asserted-by":"crossref","DOI":"10.1093\/jigpal\/5.2.287","article-title":"A polynomial translation of S4 into T and contraction free tableaux for S4","author":"Cerrito","year":"1997","journal-title":"Logic Journal of the IGPL"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0110","series-title":"Modal Logic: An Introduction","author":"Chellas","year":"1980"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0115","series-title":"Automated Reasoning with Analytic Tableaux and Related Methods","first-page":"175","article-title":"Variants of first\u2013order modal logics","author":"Cialdea Mayer","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0120","doi-asserted-by":"crossref","first-page":"249","DOI":"10.2307\/2266613","article-title":"The elimination theorem when modality is present","volume":"17","author":"Curry","year":"1952","journal-title":"Journal of Symbolic Logic"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50024-2_rf0125","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1080\/11663081.1995.10510844","article-title":"Uniform and non uniform strategies for tableaux calculi for modal logics","volume":"5","author":"Demri","year":"1995","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0130","series-title":"Automated Reasoning with Analytic Tableaux and Related Methods","first-page":"205","article-title":"Properties of embeddings from Int to S4","author":"Egly","year":"2000"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0135","series-title":"Proc. AISC","first-page":"132","article-title":"Intuitionistic proof transformation and their application to constructive program synthesis","author":"Egly","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0140","doi-asserted-by":"crossref","first-page":"59","DOI":"10.3233\/FI-1999-391204","article-title":"On intuitionistic proof transformation, their complexity and application to constructive program synthesis","volume":"39","author":"Egly","year":"1999","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0145","first-page":"152","article-title":"Tree proofs in modal logic","volume":"31","author":"Fitch","year":"1966","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0150","series-title":"Proof methods for modal and intuitionistic logics","author":"Fitting","year":"1983"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0155","first-page":"368","article-title":"Basic modal logic","volume":"Vol. 1","author":"Fitting","year":"1993"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0160","series-title":"First-Order Logic and Automated Theorem Proving","author":"Fitting","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0165","series-title":"First-Order Modal Logic","author":"Fitting","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0170","series-title":"Labelled deductive systems","author":"Gabbay","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0175","first-page":"249","article-title":"Quantification in modal logic","volume":"Vol. 2","author":"Garson","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50024-2_rf0180","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen","volume":"39","author":"Gentzen","year":"1934","journal-title":"Mathematische Zeitschrift"},{"key":"10.1016\/B978-044450813-3\/50024-2_rf0185","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/BF01201363","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen","volume":"39","author":"Gentzen","year":"1934","journal-title":"Mathematische Zeitschrift"},{"key":"10.1016\/B978-044450813-3\/50024-2_rf0190","first-page":"1934","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen","volume":"39","author":"Gentzen","year":"1934","journal-title":"Mathematische Zeitschrift"},{"key":"10.1016\/B978-044450813-3\/50024-2_rf0195","series-title":"The Collected Papers of Gerhard Gentzen","author":"Szabo","year":"1969"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0185","series-title":"Handbook of Tableaux Methods","first-page":"297","article-title":"Tableau methods for modal and temporal logics","author":"Gor\u00e9","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0190","series-title":"Theorem Proving with Analytic Tableaux and Related Methods","first-page":"79","article-title":"Labelled tableaux for multi-modal logics","author":"Governatori","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0195","series-title":"Automated Reasoning with Analytic Tableaux and Related Methods. Position Papers and Tutorials","first-page":"3","article-title":"Labelled modal sequents","author":"Governatori","year":"2000"},{"issue":"6","key":"10.1016\/B978-044450813-3\/50024-2_bb0200","doi-asserted-by":"crossref","first-page":"819","DOI":"10.1093\/logcom\/6.6.819","article-title":"A-ordered tableaux","volume":"6","author":"H\u00e4hnle","year":"1996","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0205","series-title":"From Frege to G\u00f6del: A Source Book of Mathematical Logic","first-page":"525","article-title":"Investigations in proof theory","author":"Herbrand","year":"1967"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0210","series-title":"Knowledge and Belief","author":"Hintikka","year":"1962"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0215","series-title":"An Introduction to Modal Logic","author":"Hughes","year":"1968"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0220","series-title":"A Companion to Modal Logic","author":"Hughes","year":"1984"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0225","series-title":"Stockholm Studies in Philosophy","article-title":"Provability in logic","author":"Kanger","year":"1957"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0230","first-page":"1","article-title":"Permutability of inferences in Gentzen's calculi LK and LJ","volume":"10","author":"Kleene","year":"1952","journal-title":"Memoirs of the American Mathematical Society"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0235","series-title":"14th International Conference on Automated Deduction","first-page":"131","article-title":"Deciding intuitionistic propositional logic via translation into classical logic","author":"Korn","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0240","series-title":"14th International Conference on Automated Deduction","first-page":"207","article-title":"Connection-based proof construction in linear logic","author":"Kreitz","year":"1997"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50024-2_rf0260","first-page":"88","article-title":"Connection-based theorem proving in classical and non-classical logics","volume":"5","author":"Kreitz","year":"1999","journal-title":"Journal for Universal Computer Science"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0250","series-title":"International Conference TABLEAUX-2000","first-page":"294","article-title":"Matrix-based inductive theorem proving","author":"Kreitz","year":"2000"},{"issue":"1\u20132","key":"10.1016\/B978-044450813-3\/50024-2_bb0255","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1006\/inco.2000.2913","article-title":"A uniform procedure for converting matrix proofs into sequent\u2013style systems","volume":"162","author":"Kreitz","year":"2000","journal-title":"Journal of Information and Computation"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50024-2_bb0260","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2964568","article-title":"A completeness theorem in modal logic","volume":"24","author":"Kripke","year":"1959","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0265","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1002\/malq.19630090502","article-title":"Semantic analysis of modal logic I: Normal modal propositional calculi","volume":"9","author":"Kripke","year":"1963","journal-title":"Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0270","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":"Ladner","year":"1977","journal-title":"SIAM Journal of Computation"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0275","series-title":"Handbook of Tableaux Methods","first-page":"125","article-title":"Tableau methods for modal and temporal logics","author":"Letz","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0280","first-page":"2015","article-title":"Model elimination and connection tableau procedures","volume":"Vol. II","author":"Letz","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0285","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1017\/S0027763000018055","article-title":"Eine Darstellung der intuitionistische Logik in der klassischen","volume":"7","author":"Maehara","year":"1954","journal-title":"Nagoya Mathematical Journal"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0290","series-title":"6th European Workshop on Logics in AI (JELIA-98)","first-page":"169","article-title":"A matrix characterization for MELL","author":"Mantel","year":"1998"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0295","series-title":"Proc. CADE-12","first-page":"723","article-title":"Strongly analytic tableaux for normal modal logics","author":"Massacci","year":"1994"},{"issue":"3","key":"10.1016\/B978-044450813-3\/50024-2_bb0300","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1023\/A:1006155811656","article-title":"Single step tableaux for modal logics","volume":"24","author":"Massacci","year":"2000","journal-title":"Journal of Automated Reasoning"},{"issue":"6","key":"10.1016\/B978-044450813-3\/50024-2_bb0305","doi-asserted-by":"crossref","first-page":"671","DOI":"10.1023\/A:1017948105274","article-title":"Indexed systems of sequents and cut-elimination","volume":"26","author":"Mints","year":"1997","journal-title":"Journal of Philosophical Logic"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0310","series-title":"Proc. 9th International Conference on Automated Deduction","first-page":"500","article-title":"A resolution calculus for modal logics","author":"Ohlbach","year":"1988"},{"issue":"5","key":"10.1016\/B978-044450813-3\/50024-2_bb0315","doi-asserted-by":"crossref","first-page":"691","DOI":"10.1093\/logcom\/1.5.691","article-title":"Semantics-based translation methods for modal logics","volume":"1","author":"Ohlbach","year":"1990","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0320","first-page":"1403","article-title":"Encoding two-valued nonclassical logics in classical logic","volume":"Vol. II","author":"Ohlbach","year":"2001"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0325","first-page":"147","article-title":"Corrections to our paper \u2018Gentzen method in modal calculi I\u2019","volume":"10","author":"Ohnishi","year":"1957","journal-title":"Osaka Mathematical Journal"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0330","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\/B978-044450813-3\/50024-2_bb0335","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\/B978-044450813-3\/50024-2_bb0340","series-title":"International Conference on Automated Reasoning with Analytic Tableaux and Related Methods","first-page":"307","article-title":"ilean TAP: An Intuitionistic Theorem Prover","author":"Otten","year":"1997"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0345","series-title":"Theorem Proving with Analytic Tableaux and Related Methods","first-page":"122","article-title":"A connection based proof method for intuitionistic logic","author":"Otten","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50024-2_rf0365","series-title":"5th Workshop on Theorem Proving with Analytic Tableaux and Related Methods","first-page":"244","article-title":"T-String-Unification: Unifying Prefixes in Non-Classical Proof Methods","author":"Otten","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0355","article-title":"Towards efficient prefix unification in non-classical theorem proving","author":"Otten","year":"2001","journal-title":"Technical Report AIDA-00-03, Intellectics Group, Darmstadt University of Technology"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0360","series-title":"Symposia Gaussiana, Conf. A","first-page":"225","article-title":"Loop-free construction of counter-models for intuitionistic propositional logic","author":"Pinto","year":"1995"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0365","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1111\/j.1755-2567.1960.tb00558.x","article-title":"An improved proof procedure","volume":"26","author":"Prawitz","year":"1960","journal-title":"Theoria"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0370","series-title":"Tenth Conference on Automated Deduction, Lecture Notes in Computer Science 449","first-page":"236","article-title":"Investigations into proof\u2013search in a system of first\u2013order dependent function types","author":"Pym","year":"1990"},{"issue":"1","key":"10.1016\/B978-044450813-3\/50024-2_bb0375","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"J. of the ACM"},{"issue":"5","key":"10.1016\/B978-044450813-3\/50024-2_bb0380","doi-asserted-by":"crossref","first-page":"619","DOI":"10.1093\/logcom\/2.5.619","article-title":"An Intuitionistic Predicate Logic Theorem Prover","volume":"2","author":"Sahlin","year":"1992","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0385","article-title":"Vollst\u00e4ndige Systeme modaler und institutionistischer Logik","author":"Sch\u00fctte","year":"1968"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0390","article-title":"Basic proof theory","author":"Schwichtenberg","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0395","series-title":"Proceedings of 11th International Conference on Automated Deduction","first-page":"522","article-title":"Proof search in the intuitionistic sequent calculus","author":"Shankar","year":"1992"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0400","series-title":"First-Order Logic","author":"Smullyan","year":"1968"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0405","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(79)90007-0","article-title":"Intuitionistic logic is polynomial-space complete","volume":"9","author":"Statman","year":"1979","journal-title":"Theor. Comp. Science"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0410","first-page":"225","article-title":"Intuitionistic logic","volume":"Vol. III","author":"van Dalen","year":"1986"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0415","series-title":"Proc. 5th TABLEAUX'96","first-page":"312","article-title":"Proof search in intuitionistic logic based on constraint satisfaction","author":"Voronkov","year":"1996"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0420","article-title":"A sequent calculus for intuitionistic logic with classical permutation properties","author":"Waller","year":"2001","journal-title":"Technical Report 285, Department of Computer Science, University of Oslo"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0425","series-title":"Handbook of Tableaux Methods","first-page":"255","article-title":"Tableaux for intuitionistic logics","author":"Waaler","year":"1999"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0430","series-title":"10th International Joint Conference on Artificial Intelligence","first-page":"917","article-title":"Matrix proof methods for modal logics","author":"Wallen","year":"1987"},{"key":"10.1016\/B978-044450813-3\/50024-2_bb0435","series-title":"Automated deduction in nonclassical logics","author":"Wallen","year":"1990"}],"container-title":["Handbook of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500242?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444508133500242?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,23]],"date-time":"2020-04-23T01:26:27Z","timestamp":1587605187000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444508133500242"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9780444508133"],"references-count":89,"URL":"https:\/\/doi.org\/10.1016\/b978-044450813-3\/50024-2","relation":{},"subject":[],"published":{"date-parts":[[2001]]}}}