Accepted and invited papers with slides


  • Building SMT-based Software Model Checkers: an Experience Report
    Alessandro Armando (Slides)
  • Combining Nonmonotonic Knowledge Bases with External Sources
    Thomas Eiter, Gerhard Brewka, Minh Dao-Tran, Michael Fink, Giovambattista Ianni, Thomas Krennwallner (Slides)
  • Combining Description Logics, Description Graphs, and Rules
    Boris Motik (Slides)
  • Combining Equational Reasoning
    Ashish Tiwari (Slides)


  • Superposition Modulo Linear Arithmetic --  SUP(LA)
    Ernst Althaus, Evgeny Kruglov, Christoph Weidenbach (Slides)
  • Unification modulo Homomorphic Encryption
    Siva Anantharaman, Hai Lin, Christopher Lynch, Paliath Narendran, Michael Rusinowitch (Slides)
  • Argument Filterings and Usable Rules for Simply Typed Dependency Pairs
    Takahito Aoto, Toshiyuki Yamada (Slides)
  • DL-Lite with Temporalised Concepts, Rigid Axioms and Roles
    Alessandro Artale, Roman Kontchakov, Vladislav Ryzhikov, Michael Zakharyaschev (Slides)
  • Runtime Verification Using a Temporal Description Logic
    Franz Baader, Andreas Bauer, Marcel Lippmann (Slides)
  • Axiomatization and completeness of lexicographic products of modal logics
    Philippe Balbiani (Slides)
  • Automating Theories in Intuitionistic Logic
    Guillaume Burel (Slides)
  • Taming the Complexity of Temporal Epistemic Reasoning
    Clare Dixon, Michael Fisher, Boris Konev (Slides)
  • Putting ABox Updates into Action
    Conrad Drescher, Hongkai Liu, Franz Baader, Peter Steinke, Michael Thielscher, Uwe Petersohn, Steffen Guhlemann (Slides)
  • A Declarative Agent Programming Language Based On Action Theories
    Conrad Drescher, Stephan Schiffel, Michael Thielscher (Slides)
  • Termination Modulo Combinations of Equational Theories
    Francisco Duran, Salvador Lucas, Jose Meseguer (Slides)
  • Combinations of theories for decidable fragments of first-order logic
    Pascal Fontaine (Slides)
  • Products of modal logics with diagonal constant lacking the finite model property
    Agi Kurucz (Slides)
  • Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
    Stephane Lescuyer, Sylvain Conchon (Slides)
  • Combining Instance Generation and Resolution
    Christopher Lynch, Ralph Eric McGregor (Slides)
  • Data Structures with Arithmetic Constraints: a Non-Disjoint Combination
    Enrica Nicolini, Christophe Ringeissen, Michael Rusinowitch (Slides)
  • A new collaborative scheme for computing a MUS
    Cedric Piette, Youssef Hamadi, Lakhdar Sais
  • Learning to integrate deduction and search in QBF reasoning
    Luca Pulina, Armando Tacchella (Slides)
  • Combining Theories with Shared Set Operations
    Thomas Wies, Ruzica Piskac, Viktor Kuncak (Slides)