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.