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

Carnegie Mellon University, Pittsburgh PA

Investigators

Abstract

9909952 Pfenning This 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.