Frontiers of Combining Systems: 7th International Symposium, FroCoS 2009, Trento, Italy, September 16-18, 2009. Proceedings

Description

This book constitutes the refereed proceedings of the 7th International Symposium on Frontiers of Combining Systems, FroCoS 2007, held in Trento, Italy, September 16-18, 2009. The 20 revised full papers presented were carefully reviewed and selected. The papers are organized in topical sections on combinations of logics, theories, and decision procedures; constraint solving and programming; combination issues in rewriting and programming as well as in logical frameworks and theorem proving systems. Front Matter....Pages - Building SMT-Based Software Model Checkers: An Experience Report....Pages 1-17 Combining Nonmonotonic Knowledge Bases with External Sources....Pages 18-42 Combining Description Logics, Description Graphs, and Rules....Pages 43-67 Combining Equational Reasoning....Pages 68-83 Superposition Modulo Linear Arithmetic SUP(LA)....Pages 84-99 Unification Modulo Homomorphic Encryption....Pages 100-116 Argument Filterings and Usable Rules for Simply Typed Dependency Pairs....Pages 117-132 DL-Lite with Temporalised Concepts, Rigid Axioms and Roles....Pages 133-148 Runtime Verification Using a Temporal Description Logic....Pages 149-164 Axiomatization and Completeness of Lexicographic Products of Modal Logics....Pages 165-180 Automating Theories in Intuitionistic Logic....Pages 181-197 Taming the Complexity of Temporal Epistemic Reasoning....Pages 198-213 Putting ABox Updates into Action....Pages 214-229 A Declarative Agent Programming Language Based on Action Theories....Pages 230-245 Termination Modulo Combinations of Equational Theories....Pages 246-262 Combinations of Theories for Decidable Fragments of First-Order Logic....Pages 263-278 Products of Modal Logics with Diagonal Constant Lacking the Finite Model Property....Pages 279-286 Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme....Pages 287-303 Combining Instance Generation and Resolution....Pages 304-318 Data Structures with Arithmetic Constraints: A Non-disjoint Combination....Pages 319-334 Efficient Combination of Decision Procedures for MUS Computation....Pages 335-349 Learning to Integrate Deduction and Search in Reasoning about Quantified Boolean Formulas....Pages 350-365 Combining Theories with Shared Set Operations....Pages 366-382 Back Matter....Pages -