Design, Implementation and Application of a Framework for the Formalization of Deductive Systems

9619584本项目是NSF拨款CCR-9303383的续期项目。由于计算机科学和逻辑学中对各种各样的演绎系统感兴趣，研究者和其他人已经研究了用于其规范的通用元语言，通常被称为逻辑框架。先前拨款的工作包括设计逻辑框架LF和基于LF的逻辑编程语言Elf。广泛的案例研究证实了基础生态系统和生态系统的方法的广泛适用性，并指出了本项目将解决的某些限制。这项工作包括一种用于演绎系统和元程序的模块化表示的语言，以及对框架的改进，以允许子类型、线性和内部方程推理。该项目将实现这些语言改进，建立在当前的原型以及LF和Elf的核心和模块语言实现的基础上。它还将继续探索使用LF和Elf及其改进作为表示演绎系统元定理证明的载体；也就是说，它们被用作元逻辑框架。前一笔赠款下的若干个案研究表明这种说明是可行的，但仍有更多的理论和执行工作有待完成。在长期计划中，该项目将提高执行此类证明的自动化程度，利用表征的高度抽象和LF的表达类型系统。＊＊＊

9619584 This project is a renewal of NSF Grant CCR-9303383 with the same title. Motivated by the tremendous variety of deductive systems of interest in computer science and logic, general meta-languages for their specification, often referred to as logical frameworks, have been investigated by the researcher and others. Work on the previous grant includes the design of the logical framework LF and the logic programming language Elf based on LF. Extensive case studies have confirmed the wide range of applicability of the methodology underlying LF and Elf and also pointed towards certain limitations, which this project will address. The work includes a language for modular presentation of deductive systems and meta-programs, and refinements of the framework to permit subtyping, linearity, and internal equational reasoning. The project will implement these language refinements, building on current prototypes and the core and module language implementations for LF and Elf. It will also continue to explore the use of LF and Elf and their refinements as vehicles for representing proofs of meta theorems about deductive systems; that is, their use as a meta-logical framework. A number of case studies under the previous grant indicate the feasibility of such representations, but more theoretical and implementation work remains to be done. In longer term plans, the project will increase the degree of automation of carrying out such proofs, taking advantage of the high level of abstraction of the representations and the expressive type system of LF. ***