DOHJI(ID:5025/doh001)
natural language like proof description language, part of the constructive programming system SHUTEN
References:
Y.Takayama "SHUTEN: A Constructive Programming System" JJSAI 7(4) 1989 view details
Abstract: 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 dasigned 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 they also keep the whole programming system compact.
|