## Frontiers of Combining Systems 2The International workshop 'Frontiers of Combining Systems' is the only forum that is exclusively devoted to research efforts in this interdisciplinary area. This volume contains selected, edited papers from the second installment of the workshop. The contributions range from theorem proving, rewriting and logic to systems and constraints. While there is a clear emphasis on automated tools and logics, the contributions to this volume show that there exists a rapidly expanding body of solutions of particular instances of the combination problem, and at the same time, that the issue of developing general frameworks for intergrating formalisms and systems is taking on an increasingly important position on the international research agenda. The idea of combining formal systems and algorithms has been attracting interest in areas as diverse as constraint logic programming, automated deduction, verification, information retrieval, computational linguistics, artificial intelligence, and logic. As any interesting real world system is a complex composite entity, decomposing its descriptive requirements (for design, verification, or maintenance purposes) into simpler, more restricted tasks is appealing as it is often the only plausible way of tackling complex modelling problems. A core body of notions, questions and results is beginning to emerge in the area, and we are beginning to understand the computational and logical impact of combining methods and algorithms. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

Enno Ohlebusch Technische Fakultat University of Bielefeld P O Box | 1 |

ChurchRosser Property for Conditional Rewriting Systems with Builtin | 17 |

Combining WS1S and | 39 |

Copyright | |

21 other sections not shown

### Common terms and phrases

algebras algorithm application Artificial Intelligence axioms BIS-CTRSs bitwise operations bounds built-in predicates calculus CLAM clauses combination complete component Computer Science confluence consider constraint problem constraint solvers corresponding decision procedure deduction defined Definition denote dependency pair description logics DFOL diamond lemma domain equational example expressions extended fibring finite finnat formal formulae function symbols given higher-order logic Horn clauses hybrid hybrid theory implementation induction institution integer interpretation IntTerm Isabelle/HOL Kirchner labelled language Lemma linear constant restrictions lwffs mapping modal logics modularity morphism natural numbers non-classical logics notion Nuprl operators oracle p-calculus Presburger arithmetic proof prove quasi-free structures reasoning redex relation relevance logics representation represented rewrite rule Rewriting Systems rwffs satisfies Section semantics sequent sequent systems signature simply terminating solution solvable solving specifications strategy substitution syntactic Tarlecki theorem prover tion translation TRSs unification variables WS1S