7. FroCos 2009: Trento, Italy

Invited Talks

• Alessandro Armando:
  Building SMT-Based Software Model Checkers: An Experience Report. 1-17
  
• Thomas Eiter, Gerhard Brewka, Minh Dao-Tran, Michael Fink, Giovambattista Ianni, Thomas Krennwallner:
  Combining Nonmonotonic Knowledge Bases with External Sources. 18-42
  
• Boris Motik:
  Combining Description Logics, Description Graphs, and Rules. 43-67
  
• Ashish Tiwari:
  Combining Equational Reasoning. 68-83
  

Technical Papers

• Ernst Althaus, Evgeny Kruglov, Christoph Weidenbach:
  Superposition Modulo Linear Arithmetic SUP(LA). 84-99
  
• Siva Anantharaman, Hai Lin, Christopher Lynch, Paliath Narendran, Michaël Rusinowitch:
  Unification Modulo Homomorphic Encryption. 100-116
  
• Takahito Aoto, Toshiyuki Yamada:
  Argument Filterings and Usable Rules for Simply Typed Dependency Pairs. 117-132
  
• Alessandro Artale, Roman Kontchakov, Vladislav Ryzhikov, Michael Zakharyaschev:
  DL-Lite with Temporalised Concepts, Rigid Axioms and Roles. 133-148
  
• Franz Baader, Andreas Bauer, Marcel Lippmann:
  Runtime Verification Using a Temporal Description Logic. 149-164
  
• Philippe Balbiani:
  Axiomatization and Completeness of Lexicographic Products of Modal Logics. 165-180
  
• Guillaume Burel:
  Automating Theories in Intuitionistic Logic. 181-197
  
• Clare Dixon, Michael Fisher, Boris Konev:
  Taming the Complexity of Temporal Epistemic Reasoning. 198-213
  
• Conrad Drescher, Hongkai Liu, Franz Baader, Steffen Guhlemann, Uwe Petersohn, Peter Steinke, Michael Thielscher:
  Putting ABox Updates into Action. 214-229
  
• Conrad Drescher, Stephan Schiffel, Michael Thielscher:
  A Declarative Agent Programming Language Based on Action Theories. 230-245
  
• Francisco Durán, Salvador Lucas, José Meseguer:
  Termination Modulo Combinations of Equational Theories. 246-262
  
• Pascal Fontaine:
  Combinations of Theories for Decidable Fragments of First-Order Logic. 263-278
  
• Agi Kurucz:
  Products of Modal Logics with Diagonal Constant Lacking the Finite Model Property. 279-286
  
• Stéphane Lescuyer, Sylvain Conchon:
  Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme. 287-303
  
• Christopher Lynch, Ralph Eric McGregor:
  Combining Instance Generation and Resolution. 304-318
  
• Enrica Nicolini, Christophe Ringeissen, Michaël Rusinowitch:
  Data Structures with Arithmetic Constraints: A Non-disjoint Combination. 319-334
  
• Cédric Piette, Youssef Hamadi, Lakhdar Sais:
  Efficient Combination of Decision Procedures for MUS Computation. 335-349
  
• Luca Pulina, Armando Tacchella:
  Learning to Integrate Deduction and Search in Reasoning about Quantified Boolean Formulas. 350-365
  
• Thomas Wies, Ruzica Piskac, Viktor Kuncak:
  Combining Theories with Shared Set Operations. 366-382