Frontiers of Combining Systems

1. Front Matter

   PDF

2. Invited Talk 1

   1. MetiTarski’s Menagerie of Cooperating Systems

      • Lawrence C. Paulson

      Pages 1-6

3. Inductive Theorem Proving

   1. Combining Superposition and Induction: A Practical Realization

      • Abdelkader Kersani, Nicolas Peltier

      Pages 7-22

4. Arrays and Memory Access Optimization

   1. Definability of Accelerated Relations in a Theory of Arrays and Its Applications

      • Francesco Alberti, Silvio Ghilardi, Natasha Sharygina

      Pages 23-39

   2. Verification of Composed Array-Based Systems with Applications to Security-Aware Workflows

      • Clara Bertolissi, Silvio Ranise

      Pages 40-55

   3. Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages

      • Ralf Karrenberg, Marek Košta, Thomas Sturm

      Pages 56-70

5. Approximation and Forgetting

   1. Roughening the \(\mathcal{EL}\) Envelope

      • Rafael Peñaloza, Tingting Zou

      Pages 71-86

   2. Uniform Interpolation of \(\mathcal{ALC}\)-Ontologies Using Fixpoints

      • Patrick Koopmann, Renate A. Schmidt

      Pages 87-102

   3. Abduction in Logic Programming as Second-Order Quantifier Elimination

      • Christoph Wernhard

      Pages 103-119

6. Invited Talk 2

   1. Witness Runs for Counter Machines

      • Clark Barrett, Stéphane Demri, Morgan Deters

      Pages 120-150

7. Temporal and Description Logic Techniques

   1. Decidability and Complexity via Mosaics of the Temporal Logic of the Lexicographic Products of Unbounded Dense Linear Orders

      • Philippe Balbiani, Szabolcs Mikulás

      Pages 151-164

   2. Temporal Query Answering in the Description Logic DL-Lite

      • Stefan Borgwardt, Marcel Lippmann, Veronika Thost

      Pages 165-180

   3. Verification of Golog Programs over Description Logic Actions

      • Franz Baader, Benjamin Zarrieß

      Pages 181-196

8. Invited Talk 3

   1. Specification and Verification of Linear Dynamical Systems: Advances and Challenges

      • Joël Ouaknine

      Pages 197-197

9. Theorem Proving with Theories and Sorts

   1. Obtaining Finite Local Theory Axiomatizations via Saturation

      • Matthias Horbach, Viorica Sofronie-Stokkermans

      Pages 198-213

   2. Non-cyclic Sorts for First-Order Satisfiability

      • Konstantin Korovin

      Pages 214-228

   3. Detection of First Order Axiomatic Theories

      • Guillaume Burel, Simon Cruanes

      Pages 229-244

   4. Mechanizing the Metatheory of Sledgehammer

      • Jasmin Christian Blanchette, Andrei Popescu

      Pages 245-260

10. Invited Talk 4

    1. From Resolution and DPLL to Solving Arithmetic Constraints

       • Konstantin Korovin

       Pages 261-262

11. Modal Logic and Description Logic

    1. Tableaux for Relation-Changing Modal Logics

       • Carlos Areces, Raul Fervari, Guillaume Hoffmann

       Pages 263-278

This book constitutes the refereed proceedings of the 9th International Symposium on Frontiers of Combining Systems, FroCoS 2013, held in Nancy, France, in September 2013. The 20 revised full papers presented together with 4 invited papers were carefully reviewed and selected from 33 submissions. FroCoS'13 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. Typical topics of interest include following subjects: combinations of logics such as combined predicate, temporal, modal or epistemic logics, combinations and modularity in ontologies, combination of decision, procedures, of satisfiability, procedures and of constraint solving techniques, combinations and modularity in term rewriting, integration of equational and other theories into deductive systems, combination of deduction systems and computer algebra, integration of data structures into constraint logic programming and deduction, and modularizing programs and specifications.

• complexity
• decidability
• linear temporal logic
• model checking
• term rewriting
• algorithm analysis and problem complexity

• LORIA, Inria Nancy Grand Est, Université de Lorraine, Villers-les-Nancy, France

  Pascal Fontaine

• LORIA, Inria Nancy Grand Est, Villers-lès-Nancy, France

  Christophe Ringeissen

• School of Computer Science, The University of Manchester, Manchester, UK

  Renate A. Schmidt

Policies and ethics