Frontiers of Combining Systems

1. Front Matter

   PDF

2. Invited Papers

   1. Tailoring Temporal Description Logics for Reasoning over Temporal Conceptual Models

      • Alessandro Artale, Roman Kontchakov, Vladislav Ryzhikov, Michael Zakharyaschev

      Pages 1-11

   2. Automatic Proof and Disproof in Isabelle/HOL

      • Jasmin Christian Blanchette, Lukas Bulwahn, Tobias Nipkow

      Pages 12-27

   3. Size-Change Termination and Satisfiability for Linear-Time Temporal Logics

      • Martin Lange

      Pages 28-39

3. Contributed Papers

   1. Combining Theories: The Ackerman and Guarded Fragments

      • Carlos Areces, Pascal Fontaine

      Pages 40-54

   2. On the Undecidability of Fuzzy Description Logics with GCIs and Product T-norm

      • Franz Baader, Rafael Peñaloza

      Pages 55-70

   3. The Complexity of Reversal-Bounded Model-Checking

      • Marcello M. Bersani, Stéphane Demri

      Pages 71-86

   4. Expressing Polymorphic Types in a Many-Sorted Language

      • François Bobot, Andrei Paskevich

      Pages 87-102

   5. A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints

      • Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise

      Pages 103-118

   6. Superposition Modulo Non-linear Arithmetic

      • Andreas Eggers, Evgeny Kruglov, Stefan Kupferschmid, Karsten Scheibler, Tino Teige, Christoph Weidenbach

      Pages 119-134

   7. The Modal Logic of Equilibrium Models

      • Luis Fariñas del Cerro, Andreas Herzig

      Pages 135-146

   8. Harnessing First Order Termination Provers Using Higher Order Dependency Pairs

      • Carsten Fuhs, Cynthia Kop

      Pages 147-162

   9. Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT

      • Alberto Griggio, Quoc-Sang Phan, Roberto Sebastiani, Silvia Tomasi

      Pages 163-178

   10. Controlled Term Rewriting

       • Florent Jacquemard, Yoshiharu Kojima, Masahiko Sakai

       Pages 179-194

   11. Sharing Is Caring: Combination of Theories

       • Dejan Jovanović, Clark Barrett

       Pages 195-210

   12. Modular Termination and Combinability for Superposition Modulo Counter Arithmetic

       • Christophe Ringeissen, Valerio Senni

       Pages 211-226

   13. Congruence Closure of Compressed Terms in Polynomial Time

       • Manfred Schmidt-Schauss, David Sabel, Altug Anis

       Pages 227-242

   14. Generalized and Formalized Uncurrying

       • Christian Sternagel, René Thiemann

       Pages 243-258

   15. A Semantic Account for Modularity in Multi-language Modelling of Search Problems

       • Shahab Tasharrofi, Eugenia Ternovska

       Pages 259-274

4. Back Matter

   PDF

This book constitutes the refereed proceedings of the 8th International Symposium on Frontiers of Combining Systems, FroCoS 2011, held in Saarbrücken, Germany, in October 2011. The 15 revised full papers presented together with three invited papers were carefully reviewed and selected from 22 submissions. The event builds a common forum for research activities in the general area of combination, modularization and integration of systems, with emphasis on logic-based ones, and of their practical use.

• answer-set programming
• first-order logic
• higher order rewriting
• linear arithmetic
• model checking
• algorithm analysis and problem complexity

• University of Iowa, USA

  Cesare Tinelli

• Max-Planck-Institut für Informatik, Saarbrücken, Germany

  Viorica Sofronie-Stokkermans

Policies and ethics