構成的プログラミングシステムSHUTEN
スポンサーリンク
概要
- 論文の詳細を見る
This paper presents the design and implementation of SHUTEN, a system for formal development of programs in constructive logic. The design goal is to provide a flexible and friendly programming environment in which a specification of a program can be developed gradually from incomplete ones. SHUTEN is, in a sense, a redesign of the pioneering proof development systems based on constructive logics such as Nuprl and PX as a programming tool. SHUTEN provides a natural language like proof description language called DOHJI in which proofs are developed in the backward reasoning style. DOHJI has two facilities to describe proofs easily and concisely : The lemma facility and the formula macro definition. The lemma facility, which is designed for the gradual proof development, is an extension of referring lemmas in ordinary mathematical proofs, but it allows more concise description with the help of the proof linkage mechanism of SHUTEN. By the formula macros facility, which is almost similar to those used in other proof development systems such as PX, complex formula definitions can be drastically compressed. The SHUTEN proof checker can handle incomplete proofs and points out which part of the given proof needs more refinement. In other words, the checker assures the correctness of the proof provided that the correctness of the incomplete part is assured. With these mechanism and facilities-DOHJI, the lemma facility together with the proof linkage mechanism, the formula macros definition and the sophisticated proof checker-large proofs can be developed rather easily without using automated theorem proving systems, and also they keep the whole programming system compact.
- 社団法人人工知能学会の論文
- 1992-07-01