9. TABLEAUX 2000: St Andrews, Scotland, UK

@proceedings{DBLP:conf/tableaux/2000,
  editor    = {Roy Dyckhoff},
  title     = {Automated Reasoning with Analytic Tableaux and Related Methods,
               International Conference, TABLEAUX 2000, St Andrews, Scotland,
               UK, July 3-7, 2000, Proceedings},
  booktitle = {TABLEAUX},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1847},
  year      = {2000},
  isbn      = {3-540-67697-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Invited Lectures

• Franz Baader: Tableau Algorithms for Description Logics. 1-18
• Melvin Fitting: Modality and Databases. 19-39
• Noriko H. Arai, Alasdair Urquhart: Local Symmetries in Propositional Logic. 40-51

Comparison

• Fabio Massacci, Francesco M. Donini: Design and Results of TANCS-2000 Non-classical (Modal) Systems Comparison. 52-56
• Volker Haarslev, Ralf Möller: Consistency Testing: The RACE Experience. 57-61
• Ian Horrocks: Benchmark Analysis with FaCT. 62-66
• Ullrich Hustadt, Renate A. Schmidt: MSPASS: Modal Reasoning by Translation and First-Order Resolution. 67-71
• Peter F. Patel-Schneider: TANCS-2000 Results for DLP. 72-76
• Armando Tacchella: Evaluating ^*SAT on TANCS 2000 Benchmarks. 77-81

Research Papers

• Alberto Artosi, Guido Governatori, Antonino Rotolo: A Labelled Tableau Calculus for Nonmonotonic (Cumulative) Consequence Relations. 82-97
• Arnon Avron: A Tableau System for Gödel-Dummett Logic Based on a Hypersequent Calculus. 98-111
• Matthias Baaz, Christian G. Fermüller, Helmut Veith: An Analytic Calculus for Quantified Propositional Gödel Logic. 112-126
• Diderik Batens, Joke Meheus: A Tableau Method for Inconsistency-Adaptive Logics. 127-142
• Domenico Cantone, Calogero G. Zarba: A Tableau Calculus for Integrating First-Order and Elementary Set Theory Reasoning. 143-159
• Agata Ciabattoni, Mauro Ferrari: Hypertableau and Path-Hypertableau Calculi for Some Families of Intermediate Logics. 160-174
• Marta Cialdea Mayer, Serenella Cerrito: Variants of First-Order Modal Logics. 175-189
• Stéphane Demri: Complexity of Simple Dependent Bimodal Logics. 190-204
• Uwe Egly: Properties of Embeddings from Int to S4. 205-219
• Melvin Fitting, Lars Thalmann, Andrei Voronkov: Term-Modal Logics. 220-236
• Enrico Giunchiglia, Armando Tacchella: A Subset-Matching Size-Bounded Cache for Satisfiability in Modal Logics. 237-251
• Rajeev Goré: Dual Intuitionistic Logic Revisited. 252-267
• Raymond D. Gumb: Model Sets in a Nonconstructive Logic of Partial Terms with Definite Descriptions. 268-278
• Ortrun Ibens: Search Space Compression in Connection Tableau Calculi Using Disjunctive Constraints. 279-293
• Christoph Kreitz, Brigitte Pientka: Matrix-Based Inductive Theorem Proving. 294-308
• Pedro J. Martín, Antonio Gavilanes: Monotonic Preorders for Free Variable Tableaux. 309-323
• Maarten Marx, Szabolcs Mikulás, Mark Reynolds: The Mosaic Method for Temporal Logics. 324-340
• Linh Anh Nguyen: Sequent-Like Tableau Systems with the Analytic Superformula Property for the Modal Logics KB, KDB, K5, KD5. 341-351
• David Pearce, Inman P. de Guzmán, Agustín Valverde: A Tableau Calculus for Equilibrium Entailment. 352-367
• Carla Piazza, Alberto Policriti: Towards Tableau-Based Decision Procedures for Non-Well-Founded Fragments of Set Theory. 368-382
• Riccardo Rosati: Tableau Calculus for Only Knowing and Knowing at Most. 383-397
• Stephan Schmitt: A Tableau-Like Representation Framework for Efficient Proof Reconstruction. 398-414
• Dan E. Willard: The Semantic Tableaux Version of the Second Incompleteness Theorem Extends Almost to Robinson's Arithmetic Q. 415-430

System Descriptions

• Joachim Draeger: Redundancy-Free Lemmatization in the Automated Model-Elimination Theorem Prover AI-SETHEO. 431-435
• Gernot Stenz, Andreas Wolf: E-SETHEO: An Automated³ Theorem Prover. 436-440