| 2000 | Design and Results of TANCS-2000 Non-classical (Modal) Systems Comparison. | Fabio Massacci, Francesco M. Donini |
| 2000 | The Mosaic Method for Temporal Logics. | Maarten Marx, Szabolcs Mikuls, Mark Reynolds |
| 2000 | Monotonic Preorders for Free Variable Tableaux. | Pedro J. Martn, Antonio Gavilanes |
| 2000 | Matrix-Based Inductive Theorem Proving. | Christoph Kreitz, Brigitte Pientka |
| 2000 | Search Space Compression in Connection Tableau Calculi Using Disjunctive Constraints. | Ortrun Ibens |
| 2000 | MSPASS: Modal Reasoning by Translation and First-Order Resolution. | Ullrich Hustadt, Renate A. Schmidt |
| 2000 | Benchmark Analysis with FaCT. | Ian Horrocks |
| 2000 | Consistency Testing: The RACE Experience. | Volker Haarslev, Ralf Mller |
| 2000 | Model Sets in a Nonconstructive Logic of Partial Terms with Definite Descriptions. | Raymond D. Gumb |
| 2000 | Dual Intuitionistic Logic Revisited. | Rajeev Gor |
| 2000 | A Subset-Matching Size-Bounded Cache for Satisfiability in Modal Logics. | Enrico Giunchiglia, Armando Tacchella |
| 2000 | Term-Modal Logics. | Melvin Fitting, Lars Thalmann, Andrei Voronkov |
| 2000 | Modality and Databases. | Melvin Fitting |
| 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 | Complexity of Simple Dependent Bimodal Logics. | Stphane Demri |
| 2000 | Hypertableau and Path-Hypertableau Calculi for Some Families of Intermediate Logics. | Agata Ciabattoni, Mauro Ferrari |
| 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 | An Analytic Calculus for Quantified Propositional Gdel Logic. | Matthias Baaz, Christian G. Fermller, Helmut Veith |
| 2000 | Tableau Algorithms for Description Logics. | Franz Baader |
| 2000 | A Tableau System for Gdel-Dummett Logic Based on a Hypersequent Calculus. | Arnon Avron |
| 2000 | A Labelled Tableau Calculus for Nonmonotonic (Cumulative) Consequence Relations. | Alberto Artosi, Guido Governatori, Antonino Rotolo |
| 2000 | Local Symmetries in Propositional Logic. | Noriko H. Arai, Alasdair Urquhart |
| 1999 | Strategy Parallel Use of Model Elimination with Lemmata (System Abstract). | Andreas Wolf, Joachim Draeger |