U.S.- Germany Cooperative Research: Proof Search in Logical Frameworks

9909952 Pfenne该奖项支持Frank Pfenning和卡内基梅隆大学的两名学生，他们与德国萨尔布鲁肯的德国人工智能研究所(DFKI)的Dieter Hutter合作。该项目将专注于开发一个通用的元语言(或逻辑框架)，在该框架中，各种形式推理系统可以被简洁地编码。这种合作的中心目标是进一步理解如何从特定逻辑中推广和应用冗余消除、有效实现和启发式搜索的标准技术。预期的应用包括关于编程语言和逻辑的形式化方法和归纳推理。这项工作将使软件工程和人工智能领域有可能取得新的进展。

9909952PfenningThis award supports Frank Pfenning and two students from Carnegie Mellon University in a collaboration with Dieter Hutter of the German Research Institute for Artificial Intelligence (DFKI) in Saarbruecken, Germany. The project will focus on the development of a generic meta-langauge (or logical framework) in which various systems for formal reasoning can be encoded concisely. The central objective of this collaboration is to further the understanding of how standard techniques of redundancy elimination, efficient implementation, and heuristic search from specific logics can be generalized and applied to logical frameworks. Intended applications include formal methods and inductive reasoning about programming languages and logics. This work will make possible new advances in software engineering and artificial intelligence.