Frontiers of Combining Systems: 9th International Symposium, FroCoS 2013, Nancy, France, September 18-20, 2013. Proceedings

Description

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. Front Matter....Pages - MetiTarski’s Menagerie of Cooperating Systems....Pages 1-6 Combining Superposition and Induction: A Practical Realization....Pages 7-22 Definability of Accelerated Relations in a Theory of Arrays and Its Applications....Pages 23-39 Verification of Composed Array-Based Systems with Applications to Security-Aware Workflows....Pages 40-55 Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages....Pages 56-70 Roughening the $\mathcal{EL}$ Envelope....Pages 71-86 Uniform Interpolation of $\mathcal{ALC}$ -Ontologies Using Fixpoints....Pages 87-102 Abduction in Logic Programming as Second-Order Quantifier Elimination....Pages 103-119 Witness Runs for Counter Machines....Pages 120-150 Decidability and Complexity via Mosaics of the Temporal Logic of the Lexicographic Products of Unbounded Dense Linear Orders....Pages 151-164 Temporal Query Answering in the Description Logic DL-Lite ....Pages 165-180 Verification of Golog Programs over Description Logic Actions....Pages 181-196 Specification and Verification of Linear Dynamical Systems: Advances and Challenges....Pages 197-197 Obtaining Finite Local Theory Axiomatizations via Saturation....Pages 198-213 Non-cyclic Sorts for First-Order Satisfiability....Pages 214-228 Detection of First Order Axiomatic Theories....Pages 229-244 Mechanizing the Metatheory of Sledgehammer....Pages 245-260 From Resolution and DPLL to Solving Arithmetic Constraints....Pages 261-262 Tableaux for Relation-Changing Modal Logics....Pages 263-278 Computing Minimal Models Modulo Subset-Simulation for Modal Logics....Pages 279-294 Hybrid Unification in the Description Logic $\mathcal{EL}$ ....Pages 295-310 Disproving Confluence of Term Rewriting Systems by Interpretation and Ordering....Pages 311-326 On Forward Closure and the Finite Variant Property....Pages 327-342 Term Rewriting with Logical Constraints....Pages 343-358 Back Matter....Pages -