10th International Symposium on Frontiers of Combining Systems


Co-located with Tableaux 2015 at the Computer Science building of the University of Wroclaw, Poland
September 20 - 24, 2015

Call for papers (txt)


Invited talks

Tutorials (joint with Tableaux 2015)

Accepted papers


Additional links

  • Registration / Local Information (through TABLEAUX page)
  • Tableaux 2015
  • FroCoS Series

  • Organizers

  • Carsten Lutz and Silvio Ranise (PC Chairs)
  • Hans de Nivelle (Local Organization Chair)

  • Program Committee

  • Alessandro Artale, Free University of Bolzano-Bozen, Italy
  • Franz Baader, TU Dresden, Germany
  • Clark Barrett, New York University, USA
  • Peter Baumgartner, National ICT of Australia, Australia
  • Christoph Benzmüller, Free University of Berlin, Germany
  • Thomas Bolander, Technical University of Denmark, Denmark
  • Torben Braüner, Roskilde University, Denmark
  • Sylvain Conchon, Université Paris-Sud, France
  • Clare Dixon, University of Liverpool, UK
  • François Fages, INRIA Paris-Rocquencourt, France
  • Pascal Fontaine, Université de Lorraine, Nancy, France
  • Didier Galmiche, Université de Lorraine, Nancy, France
  • Silvio Ghilardi, Università degli Studi di Milano, Italy
  • Jürgen Giesl, RWTH Aachen, Germany
  • Guido Governatori, National ICT of Australia, Australia
  • Roman Kontchakov, Birkbeck, University of London, UK
  • Till Mossakowski, University of Magdeburg, Germany
  • Christophe Ringeissen, INRIA Nancy-Grand Est, France
  • Renate Schmidt, University of Manchester, UK
  • Roberto Sebastiani, Università di Trento, Italy
  • Viorica Sofronie-Stokkermans, Universität Koblenz-Landau, Germany
  • Andrzej Szałas, University of Warsaw, Poland
  • René Thiemann, University of Innsbruck, Austria
  • Cesare Tinelli, University of Iowa, USA
  • Luca Viganò, King's College, London, UK
  • Christoph Weidenbach, Max-Planck Institut für Informatik, Saarbrücken, Germany

  • Contact

    For further informations please send an e-mail to
    Carsten Lutz (clu@uni-bremen.de) or Silvio Ranise (ranise@fbk.eu).

    Scope of conference

    In various areas of computer science, such as logic, computation, program development and verification, artificial intelligence, knowledge representation, and automated reasoning, there is an obvious need for using specialized formalisms and inference systems for selected tasks. To be usable in practice, these specialized systems must be combined with each other and integrated into general purpose systems. This has led---in many research areas---to the development of techniques and methods for the combination and integration of dedicated formal systems, as well as for their modularization and analysis.
    The International Symposium on Frontiers of Combining Systems (FroCoS) traditionally focusses on these types of research questions and activities. Like its predecessors, FroCoS 2015 seeks to offer a common forum for research in the general area of combination, modularization, and integration of systems, with emphasis on logic-based ones, and of their practical use.

    Invited talks

  • Andreas Herzig. Knowledge and action: how should we combine their logics?
  • Philipp Rümmer. Free variables and theories: revisiting rigid E-unification
  • Thomas Sturm. From Complete Elimination Procedures to Subtropical Decisions over the Reals
  • In addition, FroCoS will share the Tableaux2015 invited speaker Oliver Ray.


  • Christoph Weidenbach. Automated Reasoning Building Blocks
  • Cesare Tinelli, Andrew Reynolds, and Clark Barrett. A Taste of SMT
  • Till Mossakowski. The distributed ontology, modeling, and specification language (DOL)-Networks of theories, languages, and logics
  • Additional Tutorials are offered by the co-located Tableaux2015 conference. Please see this page for full information and abstracts.


    Topics of interest for FroCoS'15 include (but are not restricted to):
  • combinations of logics (such as higher-order, first-order, temporal, modal, description or other non-classical logics);
  • combination and integration methods in SAT and SMT solving;
  • combination of decision procedures, satisfiability procedures, constraint solving techniques, or logical frameworks;
  • combinations and modularity in ontologies;
  • integration of equational and other theories into deductive systems;
  • hybrid methods for deduction, resolution and constraint propagation;
  • hybrid systems in knowledge representation and natural language semantics;
  • combined logics for distributed and multi-agent systems;
  • logical aspects of combining and modularizing programs and specifications;
  • integration of data structures into constraint logic programming and deduction;
  • combinations and modularity in term rewriting;
  • applications of methods and techniques to the verification and analysis of information systems.

  • Important dates

  • Deadline (abstracts): 10.05.2015
  • Deadline (full papers): 13.05.2015
  • Author notification: 22.06.2015
  • Final version due: 20.07.2015
  • Workshops/Tutorials: 20.09.2015
  • Conference: 21-24.09.2015

  • Paper submission

    The program committee seeks high-quality submissions describing original work, written in English, not overlapping with published or simultaneously submitted work to a journal or conference with archival proceedings. Selection criteria include accuracy and originality of ideas, clarity and significance of results, and quality of presentation. The page limit in Springer LNCS style is 16 pages.

    Papers must be edited in LaTeX using the llncs style and must be submitted electronically as PDF files via the EasyChair system at


    For each accepted paper, at least one of the authors is required to attend the symposium and present the work. Prospective authors must register a title and an abstract ten days before the paper submission deadline. Further information about paper submissions is available at the conference website that can be found at the beginning of this call for papers.

    Publication details

    The proceedings of the symposium will be published in the Springer LNAI/LNCS series, volume number 9322.

    Accepted papers

  • Stephan Böhme and Marcel Lippman. Decidable Description Logics of Context with Rigid Roles
  • Juergen Christ and Joechen Hoenicke. Weakely Equivalent Arrays
  • Francesco Alberti, Silvio Ghilardi, and Natasha Sharygina. A new Acceleration-based Combination Framework for Array Properties
  • Gilles Dowek, Ying Jiang, and Guillaume Burel. A completion method to decide reachability in rewrite systems
  • Tianyi Liang, Nestan Tsiskaridze, Andrew Reynolds, Cesare Tinelli, and Clark Barret. A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings
  • Franz Baader, Gerhard Brewka, and Oliver Fernandez Gil. Adding Threshold Concepts to the Description Logic EL
  • Stephan Borgwardt and Rafael Penñaloza. Reasoning in Expressive Description Logics under Infinitely Valued Gödel Semantics
  • Sarah Winkler and René Thiemann. Formalizing Soundness and Completeness of Unravelings
  • Gábor Alagi and Christoph Weidenbach. NCRL-A Model Building Approach to the Bernays-Schönfinkel Fragment
  • Andreas Teucke and Christoph Weidenbach. First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation
  • Paula Chocron, Pascal Fontaine, and Christophe Ringeissen. A Rewriting Approach to the Combination of Data Structures with Bridging Theories
  • Serdar Erbatur, Deepak Kapur, Andrew M. Marshall, and Christophe Ringeissen. Unification and Matching in Hierarchical Combinations of Syntactic Theories
  • Maximilian Jaroscheck, Pablo Federico Dobal, and Pascal Fontaine. Adapting Real Quantifier Elimination Methods for Unsatisfiable Core Computations
  • Nik Sultana, Christoph Benzmüller, and Lawrence Paulson. Proofs and reconstructions
  • Amira Zaki, Slim Abdennadher, and Thom Fruehwirth. Combining Forward and Backward Propagation
  • Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahdoubi, and Jean-Marc Notin. Axiomatic constraint systems for proof search modulo theories
  • Werner Damm, Matthias Horbach, and Viorica Sofronie-Stokkermans. Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata
  • Tobias Philipp. An Expressive Model for Instance Decomposition Based Parallel SAT Solvers
  • Michael Färber and Cezary Kaliszyk. Random Forests for Premise Selection
  • Cezary Kaliszyk, Josef Urban, and Jiri Vyskocil. Lemmatization for Stronger Reasoning in Large Theories

  • Last modified: Thu Jan 8 13:43:16 CET 2015