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

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.

---

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.

---

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.
Content:
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
Abduction in Logic Programming as Second-Order Quantifier Elimination....Pages 71-86
Witness Runs for Counter Machines....Pages 87-102
Decidability and Complexity via Mosaics of the Temporal Logic of the Lexicographic Products of Unbounded Dense Linear Orders....Pages 103-119
Verification of Golog Programs over Description Logic Actions....Pages 120-150
Specification and Verification of Linear Dynamical Systems: Advances and Challenges....Pages 151-164
Obtaining Finite Local Theory Axiomatizations via Saturation....Pages 165-180
Non-cyclic Sorts for First-Order Satisfiability....Pages 181-196
Detection of First Order Axiomatic Theories....Pages 197-197
Mechanizing the Metatheory of Sledgehammer....Pages 198-213
From Resolution and DPLL to Solving Arithmetic Constraints....Pages 214-228
Tableaux for Relation-Changing Modal Logics....Pages 229-244
Computing Minimal Models Modulo Subset-Simulation for Modal Logics....Pages 245-260
Disproving Confluence of Term Rewriting Systems by Interpretation and Ordering....Pages 261-262
On Forward Closure and the Finite Variant Property....Pages 263-278
Term Rewriting with Logical Constraints....Pages 279-294
Back Matter....Pages 295-310
....Pages 311-326