Frontiers of Combining Systems

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.

Inhalt

Invited Talks.- Building SMT-Based Software Model Checkers: An Experience Report.- Combining Nonmonotonic Knowledge Bases with External Sources.- Combining Description Logics, Description Graphs, and Rules.- Combining Equational Reasoning.- Technical Papers.- Superposition Modulo Linear Arithmetic SUP(LA).- Unification Modulo Homomorphic Encryption.- Argument Filterings and Usable Rules for Simply Typed Dependency Pairs.- DL-Lite with Temporalised Concepts, Rigid Axioms and Roles.- Runtime Verification Using a Temporal Description Logic.- Axiomatization and Completeness of Lexicographic Products of Modal Logics.- Automating Theories in Intuitionistic Logic.- Taming the Complexity of Temporal Epistemic Reasoning.- Putting ABox Updates into Action.- A Declarative Agent Programming Language Based on Action Theories.- Termination Modulo Combinations of Equational Theories.- Combinations of Theories for Decidable Fragments of First-Order Logic.- Products of Modal Logics with Diagonal Constant Lacking the Finite Model Property.- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme.- Combining Instance Generation and Resolution.- Data Structures with Arithmetic Constraints: A Non-disjoint Combination.- Efficient Combination of Decision Procedures for MUS Computation.- Learning to Integrate Deduction and Search in Reasoning about Quantified Boolean Formulas.- Combining Theories with Shared Set Operations.