Frontiers of Combining Systems 组合系统前沿/会议录

This book constitutes the refereed proceedings of the 5th International Workshop on Frontiers of Combining Systems, FroCoS 2005, held in Vienna, Austria, in September 2005. The 19 revised full papers presented including 2 system descriptions were carefully reviewed and selected from 28 submissions. 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.

Logics, Theories, and Decision Procedures I
　Invited Contribution: A Comprehensive Framework for Combined　Decision Procedures
　Connecting Many-Sorted Structures and Theories Through Adjoint　Functions
　Combining Data Structures with Nonstably Infinite Theories Using　Many-Sorted Logic
　On a Rewriting Approach to Satisfiability Procedures: Extension,　Combination of Theories and an Experimental Appraisal
Interface Formalisms
　Invited Contribution: Sociable Interfaces
Logics, Theories, and Decision Procedures II
　About the Combination of Trees and Rational Numbers in a Complete　First-Order Theory
　A Complete Temporal and Spatial Logic for Distributed Systems
Constraint Solving and Programming
　Invited Contribution: Hybrid CSP Solving
　An Efficient Decision Procedure for UTVPI Constraints
　Declarative Constraint Programming with Definitional Trees
Logical Problem Analysis and Encoding I
　Logical Analysis of Hash Functions
Combination Issues in Rewriting and Programming
　Proving and Disproving Termination of Higher-Order Functions
　Proving Liveness with Fairness Using Rewriting
　A Concurrent Lambda Calculus with Futures
Compositional System Design and Refinement
　Tutorial: The ASM Method for System Design and Analysis. A Tutorial　Introduction
Logical Problem Analysis and Encoding II
　Invited Contribution: Matching Classifications via a Bidirectional　Integration of SAT and Linguistic Resources
Theorem Proving Frameworks and Systems
　Connecting a Logical Framework to a First-Order Logic Prover
　System Description: Combination of Isabelle/HOL with Automatic　Tools
　System Description: ATS: A Language That Combines Programming　with Theorem Proving
Author Index