| 2000 | A Labelled Tableau Calculus for Nonmonotonic (Cumulative) Consequence Relations. Alberto Artosi, Guido Governatori, Antonino Rotolo |
| 2000 | A Subset-Matching Size-Bounded Cache for Satisfiability in Modal Logics. Enrico Giunchiglia, Armando Tacchella |
| 2000 | A Tableau Calculus for Equilibrium Entailment. David Pearce, Inman P. de Guzmán, Agustín Valverde |
| 2000 | A Tableau Calculus for Integrating First-Order and Elementary Set Theory Reasoning. Domenico Cantone, Calogero G. Zarba |
| 2000 | A Tableau Method for Inconsistency-Adaptive Logics. Diderik Batens, Joke Meheus |
| 2000 | A Tableau System for Gödel-Dummett Logic Based on a Hypersequent Calculus. Arnon Avron |
| 2000 | A Tableau-Like Representation Framework for Efficient Proof Reconstruction. Stephan Schmitt |
| 2000 | An Analytic Calculus for Quantified Propositional Gödel Logic. Matthias Baaz, Christian G. Fermüller, Helmut Veith |
| 2000 | Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2000, St Andrews, Scotland, UK, July 3-7, 2000, Proceedings Roy Dyckhoff |
| 2000 | Benchmark Analysis with FaCT. Ian Horrocks |
| 2000 | Complexity of Simple Dependent Bimodal Logics. Stéphane Demri |
| 2000 | Consistency Testing: The RACE Experience. Volker Haarslev, Ralf Möller |
| 2000 | Design and Results of TANCS-2000 Non-classical (Modal) Systems Comparison. Fabio Massacci, Francesco M. Donini |
| 2000 | Dual Intuitionistic Logic Revisited. Rajeev Goré |
| 2000 | E-SETHEO: An Automated Gernot Stenz, Andreas Wolf |
| 2000 | Evaluating Armando Tacchella |
| 2000 | Hypertableau and Path-Hypertableau Calculi for Some Families of Intermediate Logics. Agata Ciabattoni, Mauro Ferrari |
| 2000 | Local Symmetries in Propositional Logic. Noriko H. Arai, Alasdair Urquhart |
| 2000 | MSPASS: Modal Reasoning by Translation and First-Order Resolution. Ullrich Hustadt, Renate A. Schmidt |
| 2000 | Matrix-Based Inductive Theorem Proving. Christoph Kreitz, Brigitte Pientka |
| 2000 | Modality and Databases. Melvin Fitting |
| 2000 | Model Sets in a Nonconstructive Logic of Partial Terms with Definite Descriptions. Raymond D. Gumb |
| 2000 | Monotonic Preorders for Free Variable Tableaux. Pedro J. Martín, Antonio Gavilanes |
| 2000 | Properties of Embeddings from Int to S4. Uwe Egly |
| 2000 | Redundancy-Free Lemmatization in the Automated Model-Elimination Theorem Prover AI-SETHEO. Joachim Draeger |
| 2000 | Search Space Compression in Connection Tableau Calculi Using Disjunctive Constraints. Ortrun Ibens |
| 2000 | Sequent-Like Tableau Systems with the Analytic Superformula Property for the Modal Logics KB, KDB, K5, KD5. Linh Anh Nguyen |
| 2000 | TANCS-2000 Results for DLP. Peter F. Patel-Schneider |
| 2000 | Tableau Algorithms for Description Logics. Franz Baader |
| 2000 | Tableau Calculus for Only Knowing and Knowing at Most. Riccardo Rosati |
| 2000 | Term-Modal Logics. Melvin Fitting, Lars Thalmann, Andrei Voronkov |
| 2000 | The Mosaic Method for Temporal Logics. Maarten Marx, Szabolcs Mikulás, Mark Reynolds |
| 2000 | The Semantic Tableaux Version of the Second Incompleteness Theorem Extends Almost to Robinson's Arithmetic Q. Dan E. Willard |
| 2000 | Towards Tableau-Based Decision Procedures for Non-Well-Founded Fragments of Set Theory. Carla Piazza, Alberto Policriti |
| 2000 | Variants of First-Order Modal Logics. Marta Cialdea Mayer, Serenella Cerrito |