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

9909952 Pfenning该奖项支持来自卡内基梅隆大学的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.