Automated reasoning with analytic tableaux and related methods. 11th international conference, TABLEAUX 2002, Copenhagen, Denmark, July 30 -- August 1, 2002. Proceedings (Q1613676)

The articles of this volume will be reviewed individually. In 2001, TABLEAUX was part of IJCAR 2001 (see Zbl 0968.00052). The 9th conference, TABLEAUX 2000, has been reviewed (see Zbl 0941.00032). Indexed articles: \textit{Baaz, Matthias}, Proof analysis by resolution, 1 [Zbl 1015.03509] \textit{Miller, Dale; Pimentel, Elaine}, Using linear logic to reason about sequent systems, 2-23 [Zbl 1015.03060] \textit{Baaz, Matthias; Ciabattoni, Agata}, A Schütte-Tait style cut-elimination proof for first-order Gödel logic, 24-37 [Zbl 1015.03052] \textit{Blackburn, Patrick; Marx, Maarten}, Tableaux for quantified hybrid logic, 38-52 [Zbl 1015.03014] \textit{Chetcuti-Sperandio, Nathalie}, Tableau-based automated deduction for duration calculus, 53-69 [Zbl 1015.03013] \textit{Cialdea Mayer, Marta; Limongelli, Carla}, Linear time logic, conditioned models, and planning with incomplete knowledge, 70-84 [Zbl 1015.03012] \textit{Degtyarev, Anatoli; Fisher, Michael; Konev, Boris}, A simplified clausal resolution procedure for propositional linear-time temporal logic, 85-99 [Zbl 1015.03015] \textit{Eiter, Thomas; Klotz, Volker; Tompits, Hans; Woltran, Stefan}, Modal nonmonotonic logics revisited: Efficient encodings for the basic reasoning tasks, 100-114 [Zbl 1015.03016] \textit{Ferrari, Mauro; Fiorentini, Camillo; Fiorino, Guido}, Tableau calculi for the logics of finite \(k\)-ary trees, 115-129 [Zbl 1015.03036] \textit{Giese, Martin}, A model generation style completeness proof for constraint tableaux with superposition, 130-144 [Zbl 1015.03017] \textit{Hladik, Jan}, Implementation and optimisation of a tableau algorithm for the guarded fragment, 145-159 [Zbl 1015.03011] \textit{Letz, Reinhold}, Lemma and model caching in decision procedures for quantified Boolean formulas, 160-175 [Zbl 1015.68173] \textit{Letz, Reinhold; Stenz, Gernot}, Integration of equality reasoning into the disconnection calculus, 176-190 [Zbl 1015.68172] \textit{Metcalfe, George; Olivetti, Nicola; Gabbay, Dov}, Analytic sequent calculi for Abelian and Łukasiewicz logics, 191-205 [Zbl 1016.03058] \textit{Nguyen, Linh Anh}, Analytic tableau systems for propositional bimodal logics of knowledge and belief, 206-220 [Zbl 1016.03017] \textit{Petermann, Uwe}, A confluent theory connection calculus, 221-234 [Zbl 1016.03010] \textit{Sofronie-Stokkermans, Viorica}, On uniform word problems involving bridging operators on distributive lattices, 235-250 [Zbl 1016.06005] \textit{ten Cate, Balder; Shan, Chung-chieh}, Question answering: From partitions to Prolog, 251-265 [Zbl 1016.03025] \textit{Thion, V.; Cerrito, S.; Cialdea Mayer, Marta}, A general theorem prover for quantified modal logics, 266-280 [Zbl 1016.68106] \textit{Willard, Dan E.}, Some new exceptions for the semantic tableaux version of the second incompleteness theorem, 281-297 [Zbl 1016.03062] \textit{Wirth, Claus-Peter}, A new indefinite semantics for Hilbert's epsilon, 298-314 [Zbl 1016.03057] \textit{Zarba, Calogero G.}, A tableau calculus for combining non-disjoint theories, 315-329 [Zbl 1016.03011] \textit{Habert, L.; Notin, J.-M.; Galmiche, D.}, LINK: A proof environment based on proof nets, 330-334 [Zbl 1015.68543] \textit{Stenz, Gernot}, DCTP 1. 2 -- system abstract, 335-339 [Zbl 1015.68542]