Automated reasoning with analytic tableaux and related methods. International conference, TABLEAUX 2000, St Andrews, Scotland, GB, July 3--7, 2000. Proceedings (Q1572743)

The articles of mathematical interest will be reviewed individually. The 1999 conference has been indicated (see Zbl 0915.00048). Indexed articles: \textit{Baader, Franz; Sattler, Ulrike}, Tableau algorithms for description logics, 1-18 [Zbl 0963.03015] \textit{Fitting, Melvin}, Modality and databases, 19-39 [Zbl 0963.03028] \textit{Arai, Noriko H.; Urquhart, Alasdair}, Local symmetries in propositional logic, 40-51 [Zbl 0963.03012] \textit{Massacci, Fabio; Donini, Francesco M.}, Design and results of TANCS-2000 non-classical (modal) systems comparison, 52-56 [Zbl 0963.68518] \textit{Haarslev, Volker; Möller, Ralf}, Consistency testing: The RACE experience, 57-61 [Zbl 0963.68517] \textit{Horrocks, Ian}, Benchmark analysis with FaCT, 62-66 [Zbl 0963.68516] \textit{Hustadt, Ullrich; Schmidt, Renate A.}, MSPASS: Modal reasoning by translation and first-order resolution, 67-71 [Zbl 0963.68522] \textit{Patel-Schneider, Peter F.}, TANCS-2000 results for DLP, 72-76 [Zbl 0963.68531] \textit{Tacchella, Armando}, Evaluating *SAT on TANCS 2000 benchmarks, 77-81 [Zbl 0963.68520] \textit{Artosi, Alberto; Governatori, Guido; Rotolo, Antonino}, A labelled tableau calculus for nonmonotonic (cumulative) consequence relations, 82-97 [Zbl 0963.03005] \textit{Avron, Arnon}, A tableau system for Gödel-Dummett logic based on a hypersequent calculus, 98-111 [Zbl 0963.03008] \textit{Baaz, Matthias; Fermüller, Christian; Veith, Helmut}, An analytic calculus for quantified propositional Gödel logic, 112-126 [Zbl 0963.03075] \textit{Batens, Diderik; Meheus, Joke}, A tableau method for inconsistency-adaptive logics, 127-142 [Zbl 0963.03007] \textit{Cantone, Domenico; Zarba, Calogero G.}, A tableau calculus for integrating first-order and elementary set theory reasoning, 143-159 [Zbl 0963.03018] \textit{Ciabattoni, Agata; Ferrari, Mauro}, Hypertableau and path-hypertableau calculi for some families of intermediate logics, 160-174 [Zbl 0963.03017] \textit{Mayer, Marta Cialdea; Cerrito, Serenella}, Variants of first-order modal logics, 175-189 [Zbl 0963.03030] \textit{Demri, Stéphane}, Complexity of simple dependent bimodal logics, 190-204 [Zbl 0963.03076] \textit{Egly, Uwe}, Properties of embeddings from Int to S4, 205-219 [Zbl 0963.03077] \textit{Fitting, Melvin; Thalmann, Lars; Voronkov, Andrei}, Term-modal logics, 220-236 [Zbl 0963.03029] \textit{Giunchiglia, Enrico; Tacchella, Armando}, A subset-matching size-bounded cache for satisfiability in modal logics, 237-251 [Zbl 0963.68178] \textit{Goré, Rajeev}, Dual intuitionistic logic revisited, 252-267 [Zbl 0963.03042] \textit{Gumb, Raymond D.}, Model sets in a nonconstructive logic of partial terms with definite descriptions, 268-278 [Zbl 0963.03046] \textit{Ibens, Ortrun}, Search space compression in connection tableau calculi using disjunctive constraints, 279-293 [Zbl 0963.68189] \textit{Kreitz, Christoph; Pientka, Brigitte}, Matrix-based inductive theorem proving, 294-308 [Zbl 0963.68185] \textit{Martín, Pedro J.; Gavilanes, Antonio}, Monotonic preorders for free variable tableaux, 309-323 [Zbl 0963.68186] \textit{Marx, Maarten; Mikulás, Szabolcs; Reynolds, Mark}, The mosaic method for temporal logics, 324-340 [Zbl 0963.03025] \textit{Nguyen, Linh Anh}, Sequent-like tableau systems with the analytic superformula property for the modal logics \(KB\), \(KDB\), \(K5\), \(KD5\), 341-351 [Zbl 0963.03031] \textit{Pearce, David; de Guzmán, Immaculada P.; Valverde, Augustín}, A tableau calculus for equilibrium entailment, 352-367 [Zbl 0963.03045] \textit{Piazza, Carla; Policriti, Alberto}, Towards tableau-based decision procedures for non-well-founded fragments of set theory, 368-382 [Zbl 0963.03019] \textit{Rosati, Riccardo}, Tableau calculus for only knowing and knowing at most, 383-397 [Zbl 0963.03016] \textit{Schmitt, Stephan}, A tableau-like representation framework for efficient proof reconstruction, 398-414 [Zbl 0963.03009] \textit{Willard, Dan E.}, The semantic tableaux version of the second incompleteness theorem extends almost to Robinson's arithmetic \(Q\), 415-430 [Zbl 0963.03078] \textit{Draeger, Joachim}, Redundancy-free lemmatization in the automated model-elimination theorem prover AI-SETHEO, 431-435 [Zbl 0963.68535] \textit{Stenz, Gernot; Wolf, Andreas}, E-SETHEO: An automated\(^3\) theorem prover, 436-440 [Zbl 0963.68519]