Symposium on Frontiers of Combining Systems and Workshop on First-Order Theorem Proving

这是一份支持第六届组合系统前沿研讨会（FroCoS）和第六届一阶定理证明国际研讨会（FTP）的提案，该研讨会将于2007年9月10日至13日在利物浦大学举行。FroCoS成立于1996年，已成为致力于计算机科学和人工智能中逻辑与系统结合研究的主要科学会议。其目的是汇集来自不同领域的研究组合问题的研究人员，以促进富有成效的互动和通用技术和方法的发展，以组合和集成特殊的正式定义系统和逻辑，以及复杂系统的分析和模块化。在FroCoS上展示的主题包括约束系统和决策过程的组合，模态、时间和认知逻辑的组合及其应用，分布式和多智能体系统，软件规范和本体的模块化，以及可满足性模理论。FTP系列研讨会的目的是将对一阶定理证明的各个方面感兴趣的研究人员聚集在一起，他们将在各自领域的前沿展示工作。鉴于一阶定理证明的各种模型理论、证明理论和实践方面以及它的许多应用领域，FTP涵盖了广泛的主题。例如，一阶逻辑的推理方法，决策程序和模型构建，逻辑和系统的组合，推理模理论，以及应用和系统。从两个系列事件所讨论的主题的描述中可以明显看出，FroCoS和FTP的共同兴趣是逻辑、理论和决策程序以及可满足模理论的结合。正是这些共同的兴趣促使我们在同一地点举办活动。

This is a proposal for support for the 6th Symposium of Frontiers of Combining Systems (FroCoS)and the 6th International Workshop on First-order theorem Proving (FTP) which will be held on10th-13th September 2007 at the University of Liverpool.Founded in 1996, FroCoS has become the main scientific meeting devoted to research on combining logics and systems in computer science and artificial intelligence. Its aim is to bring together researchers from various areas working on combination problems in order to promote fruitful interaction and development of generic techniques and methods for combination andintegration of special formally defined systems and logics, as well as for the analysis and modularisation of complex systems. Examples of topics presented at FroCoS are combinations of constraint systems and decision procedures, combinations of modal, temporal and epistemic logics and their applications indistributed and multi-agent systems, modularity in software specification and ontologies, and satisfiability modulo theories.The aim of the FTP workshop series is to bring together researchers interested in all aspects of first-order theorem proving, who will present work at the cutting edge of their field. Given the various model theoretical, proof theoretical and practical aspects of first-order theorem proving as well as its many areas of application, FTP covers a wide range of topics. For example, reasoning methods for first-order logic, decision procedures and model building, combinations of logics and systems, reasoning modulo theories, and applications and systems.As is evident from the description of the topics addressed by the two series of events, common interests of FroCoS and FTP are the combination of logics, theories and decision procedures as well as satisfiability modulo theories. It is these common interests that motivate us to co-locate the events.