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

演绎系统形式化框架的设计、实现和应用

• 批准号: 9619584
• 负责人: Frank Pfenning
• 金额: $ 16万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1997
• 资助国家: 美国
• 起止时间: 1997-08-01 至 1999-10-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9619584&HistoricalAwards=false
• 关键词: Design; Implementation; Application; Framework; Formalization

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. ***

9619584该项目是具有相同标题的NSF Grant CCR-9303383的延续。受计算机科学和逻辑中各种各样的演绎系统的影响，研究人员和其他人研究了用于其规范的通用元语言，通常称为逻辑框架。上一个资助的工作包括设计逻辑框架LF和基于LF的逻辑编程语言Elf。广泛的案例研究证实了作为LF和Elf基础的方法的广泛适用性，也指出了本项目将解决的某些局限性。这项工作包括一个语言的演绎系统和元程序的模块化表示，和细化的框架，允许子类型，线性和内部方程推理。该项目将实现这些语言改进，建立在当前的原型和LF和Elf的核心和模块语言实现的基础上。它还将继续探索使用LF和Elf及其改进作为车辆代表的演绎系统的Meta定理的证明，也就是说，它们作为一个元逻辑框架的使用。根据以前的赠款进行的一些案例研究表明，这种陈述是可行的，但仍有更多的理论和执行工作要做。在长期计划中，该项目将提高进行此类证明的自动化程度，利用LF的表示和表达类型系统的高度抽象。 ***