14. TABLEAUX 2005: Koblenz, Germany

Invited Talks

• Diego Calvanese:
  Query Processing in Peer-to-Peer Systems: An Epistemic Logic Approach. 1
  
• Ian Horrocks:
  Description Logics in Ontology Applications. 2-13
  
• Hans Jürgen Ohlbach:
  Automated Reasoning in the Context of the Semantic Web. 14-14
  
• Erik Rosenthal:
  Formal Versus Rigorous Mathematics: How to Get Your Papers Published. 15-32
  

Research Papers

• Roger Antonsen, Arild Waaler:
  Consistency of Variable Splitting in Free Variable Systems of First-Order Logic. 33-47
  
• Serge Autexier:
  On the Dynamic Increase of Multiplicities in Matrix Proof Methods for Classical Higher-Order Logic. 48-62
  
• Davide Bresolin, Angelo Montanari:
  A Tableau-Based Decision Procedure for Right Propositional Neighborhood Logic. 63-77
  
• James Brotherston:
  Cyclic Proofs for First-Order Logic with Inductive Definitions. 78-92
  
• Domenico Cantone, Calogero G. Zarba:
  A Tableau-Based Decision Procedure for a Fragment of Graph Theory Involving Reachability and Acyclicity. 93-107
  
• Tobias Gedell:
  Embedding Static Analysis into Tableaux and Sequent Based Frameworks. 108-122
  
• Martin Giese:
  A Calculus for Type Predicates and Type Coercion. 123-137
  
• Rajeev Goré, Linh Anh Nguyen:
  A Tableau Calculus with Automaton-Labelled Formulae for Regular Grammar Logics. 138-152
  
• Swen Jacobs, Uwe Waldmann:
  Comparing Instance Generation Methods for Automated Reasoning. 153-168
  
• Ken Kaneiwa, Riichiro Mizoguchi:
  An Order-Sorted Quantified Modal Logic for Meta-ontology. 169-184
  
• Tatjana Lutovac, James Harland:
  A Redundancy Analysis of Sequent Proofs. 185-200
  
• Carsten Lutz, Maja Milicic:
  A Tableau Algorithm for Description Logics with Concrete Domains and GCIs. 201-216
  
• Swaha Miller, David A. Plaisted:
  The Space Efficiency of OSHL. 217-230
  
• Neil V. Murray, Erik Rosenthal:
  Efficient Query Processing with Compiled Knowledge Bases. 231-244
  
• Jens Otten:
  Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic. 245-261
  
• Sorin Stratulat:
  Automatic 'Descente Infinie' Induction Reasoning. 262-276
  
• Yoshinori Tanabe, Koichi Takahashi, Mitsuharu Yamamoto, Akihiko Tozawa, Masami Hagiya:
  A Decision Procedure for the Alternation-Free Two-Way Modal µ-Calculus. 277-291
  
• Dan E. Willard:
  On the Partial Respects in Which a Real Valued Arithmetic System Can Verify Its Tableaux Consistency. 292-306
  

System Descriptions

• Marta Cialdea Mayer, Carla Limongelli, Andrea Orlandini, Valentina Poggioni:
  Pdk: The System and Its Language. 307-311
  
• Philipp Correll, Gernot Stenz:
  Proof Output and Transformation for Disconnection Tableaux. 312-317
  
• Olivier Gasquet, Andreas Herzig, Dominique Longin, Mohamad Sahade:
  LoTREC: Logical Tableaux Research Engineering Companion. 318-322
  
• Thorsten Liebig, Michael Halfmann:
  A Tableau-Based Explainer for DL Subsumption. 323-327
  
• Nicola Olivetti, Gian Luca Pozzato:
  CondLean 3.0: Improving CondLean for Stronger Conditional Logics. 328-332
  
• Thomas Raths, Jens Otten, Christoph Kreitz:
  The ILTP Library: Benchmarking Automated Theorem Provers for Intuitionistic Logic. 333-337
  
• Gernot Stenz:
  Unit Propagation in a Tableau Framework. 338-342