Abstract:A constructive proving system and the method of combining deduction with knowledge are presented for program synthesis. The synthesis of nondeterministic logic programs is discussed. An example of synthesis of Prolog program "append" is given to illustrate our method.

Abstract:With the rapid growth of text database applications, the research of text access methods has become one of the most interesting topics in database area. According to the characters of Chinese office environment, this paper proposes a new text data base retrieval method which organizes the word signature file in the light of their superimposed coding signature. The method has no false drop that is unavoidable in other signature file methods. So it does not need to scan the full text obtained by searching the signature index .When aqiery is processed,only range scan to the signature file is required.Therefore,within a rather wide scope,the performance of our method is approximate to the inversion which is the fastest one among all the text access methods.In the meantime,it also maintains the merit of fitting dynamic information retrieval environment,that can not be found in other kinds of text access method.

Abstract:In this paper, we introduce the concepts of λ-implying, λ-strong implying, λ-weak logical consequence and λ-logical consequence. We prove that λ-resolvent of C₁ and C₂ is a λ-logical consequence of (C₁∧C₂) and compleieness theorem of λ-resolution.

Abstract:A programming method for supporting software understanding and reusing is presented in this paper, and a prototype system URS-1 to implement this method is also outlined.

Abstract:SBMTP(Simulate Boyer-Moore Theorem Prover) system is a theorem proving system which is implemented on microcomputer IBM-PC-386 by GCLISP language. The concepts and theoretical basis of the system are computational logic by Boyer and Moore. SBMTP is made up of three parts mainly: knowledge base management subsystem, theorem proving subsystem and interrupt recovery subsystem. Knowledge base management subsystem includes a fundamental knowledge base and a series of knowledge base construction tools. User can organize flexibly his knowledge base in accordance with specific requirements. Theorem proving subsystem employs a heuristic method for reasoning to complete proof. Interrupt recovery subsystem provides powerful recovery ability when proof process gets interrupted. This subsystem improves proof efficiency of the system.

Abstract:XYZ System is a CASE environment based on temporal logic and conforming to various ways of programming such as programming with HLL, hierarchical specification or production rules, sequential or concurrent, textual or graphical, etc. All these programming paradigms can be unified with a uniform framework of a temporal logic language. The system is designed with the idea to keep good balance between the theoretical rationalism and the engineering pragmatism. In this paper, this idea is illustrated from philosophical point of view.

Abstract:This paper discusses the approaches and problems of inductive program synthesis in software automation. The design background and implementation methods of an inductive program synthesizer NDIPS are proposed and the key techniques of automatic program induction adopted in the system are emphasized.