• 主题
高级搜索  >
历史搜索 清空历史
首页> 美国政府科技报告 >Course on Normalization.
【24h】

Course on Normalization.

机译：规范化课程。

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

The aim of this course is to present a basic technique from proof theory, Gentzen's normalization for natural deduction systems, and to discuss some of its applications. By normalization we mean a collection of algorithms transforming a given derivation into a certain normal form. A derivation is called normal if it does not contain any detour or - in Gentzen's terminology - cut, i.e. an application of an introduction rule immediately followed by an application of an elimination rule. Such normalization algorithms are useful because they allow one to straighten out complex derivations and in this way extract hidden information. We will treat many applications which demonstrate this, e.g. the subformula principle, Herbrand's theorem, the interpolation theorem, and an exact characterization of the initial cases of transfinite induction provable in arithmetic. From the computer science point of view, an even more interesting field of application for normalization algorithms is the possibility to extract the constructive content of a maybe complex mathematical argument. Such algorithms can yield verified programs from derivations proving that certain specifications can be fulfilled. Of course, the feasibility of programs obtained in this way will depend to a large extent on a good choice of the derivation, which should be done on the basis of a good idea for an algorithm. However, in this approach it is possible to use ordinary mathematical machinery for the development of programs. (kr)

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号