TABLEAUX 2015

Lecture Room 119A/B
Instytut Informatyki
Ulica Joliot Curie 15, Wrocław, Poland

Monday, September 21

  12:30-13:55 Lunch
  13:55-14:00 (Shared with FroCoS) Start of TABLEAUX and FroCoS
    Hans de Nivelle (Conference Chair)
 14:00-15:30 (Shared with FroCoS) Session 11 (Chair: Hans de Nivelle)
 14:00 Invited Talk: From Complete Elimination Procedures to Subtropical Decisions over the Reals
    Thomas Sturm
  15:00 An Expressive Model for Instance Decomposition-Based Parallel SAT Solvers
  Tobias Philipp
  15:30-16:00 Coffee Break
  16:00-18:00 Session 12 (Chair: Didier Galmiche)
  16:00 Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations
    Taus Brock-Nannestad, Kaustuv Chaudhuri
  16:30 Proof Search in Natural Deduction Calculus for Classical Propositional Logic
    Camillo Fiorentini, Mauro Ferrari
  17:00 Efficient Low-Level Connection Tableaux
    Cezary Kaliszyk
  17:30 The Proof Certifier "Checkers"
  Giselle Reis, Tomer Libal, Zakaria Chihani

Tuesday, September 22

 09:00-10:30 Session 21 (Chair: Cláudia Nalon)
 09:00 Invited Talk: Coherentisation of First-Order Logic
    Roy Dyckhoff
  10:00 Linear Nested Sequents, 2-Sequents and Hypersequents
    Björn Lellmann
  10:30-11:00 Coffee Break
 11:00-12:30 (Shared with FroCoS) Session 22 (Chair: Franz Baader)
  11:00 Integrating Simplex with Tableaux
    David Delahaye, Guillaume Bury
  11:30 First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation
  Andreas Teucke, Christoph Weidenbach
  12:00 Second-Order Quantifier Elimination on Relational Monadic
  Formulas — A Basic Method and Some Less Expected Applications
  Christoph Wernhardt
  12:30-14:00 Lunch
  14:00-15:30 Session 23 (Chair: Jens Otten)
  14:00 Realization Theorems for Justification Logics: Full Modularity
    Annemarie Borg, Roman Kuznets
  14:30 A Dynamic Logic with Traces and Coinduction
    Richard Bubel, Crystal Chang Din, Reiner Hähnle, Keiko Nakata
  15:00 A Propositional Tableaux Based Proof Calculus for Reasoning with Default Rules
    Valentin Cassano, Carlos Gustavo Lopez Pombo, Tom Maibaum
  15:30-16:00 Coffee Break
  16:00-17:30 Session 24 (Chair: Ullrich Hustadt)
  16:00 An Internal Calculus for Lewis Counterfactual Logics
    Nicola Olivetti, Gian Luca Pozzato
  16:30 A Tableau for Bundled Strategies
    John Christopher McCabe-Dansted, Mark Alexander Reynolds
  17:00 On Enumerating Query Plans Using Analytic Tableau
    David Toman, Grant Weddell

Wednesday, September 23

  09:00-10:30 (Shared with FroCoS) Session 31 (Chair: Roy Dyckhoff)
  09:00 Invited Talk: Symbolic Support for Scientific Discovery in Systems Biology
    Oliver Ray
  10:00 Mīmāṃsā Deontic Logic: Proof Theory and Applications
  Agata Ciabattoni, Elisa Freschi, Björn Lellmann, Francesco Antonio Genco
  10:30-11:00 Coffee Break
 11:00-12:30 (Shared with FroCoS) Session 32 (Chair: Gilles Dowek)
  11:00 Axiomatic Constraint Systems for Proof Search Modulo Theories
    Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand,
    Assia Mahdoubi, Jean-Marc Notin
  11:30 Disproving Inductive Entailments in Separation Logic via Base Pair Approximation
  James Brotherston, Nikos Gorogiannis
  12:00 Proofs and Reconstructions
  Nik Sultana, Christoph Benzmüller, Lawrence Paulson
  12:30-14:00 Lunch
  14:00-15:30 Session 33 (Chair: Reiner Hähnle)
  14:00 A Modal-Layered Resolution Calculus for K
    Cláudia Nalon, Ullrich Hustadt, Clare Dixon
  14:30 Modal Tableau Systems with Blocking and Congruence Closure
    Renate Schmidt, Uwe Waldmann
  15:00 Ordered Resolution for Coalition Logic
    Ullrich Hustadt, Paul Gainer, Clare Dixon, Cláudia Nalon, Lan Zhang
  15:30-16:00 Coffee Break
  16:00-17:00 TABLEAUX/FroCoS Joint Business Meeting
  18.00-23:59 Tour of Muzeum Narodowe + Banquet

Thursday, September 24

 09:30-10:30 Session 41 (Chair: Andrei Popescu)
 09:30 Invited Talk: On a (Quite) Universal Theorem Proving Approach and its Application in Metaphysics
    Christoph Benzmüller
  10:30-11:00 Coffee Break
 11:00-12:35 Session 42 (Chair: Andrei Popescu)
  11:00 Efficient Algorithms for Bounded Rigid E-Unification
    Peter Backeman, Philipp Rümmer
  11:30 Generalized Qualitative Spatio-Temporal Reasoning: Complexity and Tableau Method
  Michael Sioutis, Jean François Condotta, Yakoub Salhi, Bertrand Mazure
  12:00 A Sequent Calculus for Preferential Conditional Logic Based on Neighbourhood Semantics
  Nicola Olivetti, Sara Negri
  12:30-12:35 End of Conference
    Hans de Nivelle (PC Chair)
  12:35-14:00 Lunch