Automated Reasoning with Analytic Tableaux and Related Methods

1. Front Matter

   Pages I-XVI

   PDF

2. Tableaux Calculi

   1. Front Matter

      Pages 1-1

      PDF

   2. Invited Talk: Coherentisation of First-Order Logic

      • Roy Dyckhoff

      Pages 3-5

   3. A Propositional Tableaux Based Proof Calculus for Reasoning with Default Rules

      • Valentín Cassano, Carlos Gustavo Lopez Pombo, Thomas S. E. Maibaum

      Pages 6-21

   4. A Tableau for Bundled Strategies

      • John McCabe-Dansted, Mark Reynolds

      Pages 22-37

   5. Modal Tableau Systems with Blocking and Congruence Closure

      • Renate A. Schmidt, Uwe Waldmann

      Pages 38-53

   6. Generalized Qualitative Spatio-Temporal Reasoning: Complexity and Tableau Method

      • Michael Sioutis, Jean-François Condotta, Yakoub Salhi, Bertrand Mazure

      Pages 54-69

   7. Efficient Algorithms for Bounded Rigid E-unification

      • Peter Backeman, Philipp Rümmer

      Pages 70-85

   8. Integrating Simplex with Tableaux

      • Guillaume Bury, David Delahaye

      Pages 86-101

   9. Efficient Low-Level Connection Tableaux

      • Cezary Kaliszyk

      Pages 102-111

3. Sequent Calculus

   1. Front Matter

      Pages 113-113

      PDF

   2. A Sequent Calculus for Preferential Conditional Logic Based on Neighbourhood Semantics

      • Sara Negri, Nicola Olivetti

      Pages 115-134

   3. Linear Nested Sequents, 2-Sequents and Hypersequents

      • Björn Lellmann

      Pages 135-150

4. Resolution

   1. Front Matter

      Pages 151-151

      PDF

   2. Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations

      • Taus Brock-Nannestad, Kaustuv Chaudhuri

      Pages 153-168

   3. Ordered Resolution for Coalition Logic

      • Ullrich Hustadt, Paul Gainer, Clare Dixon, Cláudia Nalon, Lan Zhang

      Pages 169-184

   4. A Modal-Layered Resolution Calculus for K

      • Cláudia Nalon, Ullrich Hustadt, Clare Dixon

      Pages 185-200

   5. The Proof Certifier Checkers

      • Zakaria Chihani, Tomer Libal, Giselle Reis

      Pages 201-210

5. Other Calculi

   1. Front Matter

      Pages 211-211

      PDF

   2. Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics

      • Christoph Benzmüller

      Pages 213-220

This book constitutes the refereed proceedings of the 24th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2015, held in Wroclaw, Poland, in September 2015. 
The 19 full papers and 2 papers presented in this volume were carefully reviewed and selected from 34 submissions. They are organized in topical sections named: tableaux calculi; sequent calculus; resolution; other calculi; and applications. 

• Automated reasoning
• Computational complexity
• Linear arithmetic
• Modal logic
• Proof checking
• Coherent logic
• Computational geometry
• Coq
• Description logic
• general simplex algorithm
• intermediate logic
• logic of proofs
• normal modal logics
• proof theory
• qualitative spatiotemporal logic
• resolution method
• spatiotemporal logic
• tableau method
• tableaux
• theorem prover

• Uniwersytet Wrocławski, Wrocław, Poland

  Hans De Nivelle

Policies and ethics