http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
崔德熙 동국대학교 자연과학연구소 1984 자연과학연구 논문집 Vol.4 No.-
本 論文는 data type 定義技量을 包含한 programming言語의 意味를 明確하게 하기 위한 問題를 다룬다. 이와같은 programming 言語를 定義하는데 있어서 나타난 基本問題는 data type 定義에 주어지는 意味인 것이다. 本 論文에서 data type의 意味를 定義하고자 試圖했으며, typed lambda calculus extention의 定義에 이를 應用한다. 또한 위 programming 言漁가 strongly typed되여 있음을 定理로써 證明한다. This paper considers the general problem of specifying the meaning of programming language which include data type definition facilities. The fundamental question posed in attempting to define such hanguage is what meaning should be given to a data type deficition. In this paper, we describe a new approach to defining the meaning of data type and give its application to the definition of a typed lambda calculus extension. We also prove a theorem stating that our language is strongly typed.
Abstract Data Types Specification and Program Verification
崔德熙 東國大學校 1981 論文集 Vol.20 No.-
本 論文은 Abstract Data Types의 Specification과 Data Representation에 關한 硏究이다. 이에 關해서 다음 두가지로 接近하였다. (1) Abstract Data types의 Specification에 關한 公理論的 接近과 Data Representation에 關한 理論的인 擴張. (2) Abstract Data Types를 다룬 Program의 證明 이들을 簡單한 Program 事例의 Specification과 解析을 通해서 考察하였다.
최덕희 동국대학교 자연과학연구소 1990 자연과학연구 논문집 Vol.10 No.-
본 논문은 Fuzzy 理論이 있어서의 導出集合의 성질을 유도한 것이다. 그 성질에 의해서 理論的歸結의 애매함을 감소시킬 수 있으므로서, Fuzzy 推論이 항상 의미있는 推論이 될 수 있음을 보일 것이다. Fuzzy 反駁節次에 있어서, 前提와 推論結果는 모두 완전하지는 않지만 Fuzzy 導出에 있어서의 Fuzzy 反駁節次는 완전함을 밝힐 것이다. This paper will introduce some properties of resolutions in fuzzy logic. By those properties, a fuzzy inference will always be significant because it can be seen a procedure that will reduce the ambiguity of a logical consquence. Though the promises and conclutions as well as the inferential results are all incomplete in the fuzzy refutational procedure, we can prove that the fuzzy refutation procedure based on the fuzzy resolution pronciple is complete.
崔德熙 동국대학교 자연과학연구소 1986 자연과학연구 논문집 Vol.6 No.-
導出에 依한 定理證明에 關해서는 지금까지 많이 提案되었으나, 實際로 效果的인 方法은 問題의 特性에 依存하므로 여러가지 方法으로 表元할 수 있어야 한다. 本 論文에서 이와 같은 目的으로 programming system을 構成한다. System은 다음 다섯가지의 函數郡으로 構成한다. (1)節List로부터 節의 짝을 추출하는 函數 (2)節List를 처리하는 函數 (3)導出, 簡約形等을 實行하는 函數 (4)(2),(3)의 函數를 도와주는 補助函數 (5)initialize난 制御하기 위한 函數 本 system을 使用해서, 지금까지 알려져 있는 여러가지 戰略을 쉽게 具現할 수 있고, 또한 새 戰略의 效率性을 評價할 수 있을 것이다. 나아가서 本 system은 interactive system의 擴張을 考慮하였다. Many strategies have been proposed for the resolution theorem provers. But there is need for utilizing these various kind of strategies in practical theorem proving programs, because the dffectiveness of each strategy depends on the character of a problem. This paper presents a programming system which satisfies the need. The system is composed of five groups of functions as follows : 1.Extracting a pair of clauses from lists of clauses 2.Handling a list of clauses 3.Executing resolution, factoring etc. 4.Subsidiary functions which are used together with (2) or (3) functions. 5.Initialization and contral function. Using this systems, users can easily implement a large number of known strategies, and can also evaluate the effectiveness fo a new strategy. Another feature of this system is that it is designed in consideration of the extensibility to an interactive system.