跳到主要內容

臺灣博碩士論文加值系統

(44.200.194.255) 您好!臺灣時間:2024/07/15 01:21
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果 :::

詳目顯示

我願授權國圖
: 
twitterline
研究生:龔化中
研究生(外文):GONG, HUA-ZHONG
論文名稱:重寫理論之發散問題研究
指導教授:林一鵬林一鵬引用關係
指導教授(外文):LIN, YI-PEN
學位類別:碩士
校院名稱:國立臺灣大學
系所名稱:資訊科學研究所
學門:工程學門
學類:電資工程學類
論文種類:學術論文
論文出版年:1989
畢業學年度:77
語文別:中文
論文頁數:41
中文關鍵詞:重寫理論發散性高次元結構數學歸納法一階邏輯高階
外文關鍵詞:TERM-REWRTING-THEORYDIVERGENCEFIRST-ORDER-LOGICSECOND-ORDER-LOGIC
相關次數:
  • 被引用被引用:0
  • 點閱點閱:166
  • 評分評分:
  • 下載下載:0
  • 收藏至我的研究室書目清單書目收藏:1
本篇論文共包含下列幾項重點:
1.找出並證明重寫系統“發散”的充要條件。
2.提出在電腦證明中使用“數學歸納法”的新觀念與方法。
3.提出“高次元樹狀結構”之概念,並利用其來表示歸納得來的定理。
4.定義一種“高次元重寫系統”該系統能使很多原本會“發散”的問題收斂。
重寫系統(TERM REWRITING SYSTEM)的基本原理,是將一組等式(EQUATION )轉換
成相對的一組重寫規則,然後我們就可以利用那組重寫規則來證明定理。但在轉換的
過程中,常常會產生無數的新規則,使得這個過程無法停止。所以系統的發散性(DI
VERGENCE)在重寫理論中非常重要。
在研究的過程中,我們找到了一個重要的定理,它告訴我們重寫發散系統與否的充要
條件。由此定理,我們了解到如果想要解決這個問題,一般的樹狀結構是不夠的,我
們必需要定義一個新的高次元結構。這種結構只需一個就能表示無窮多個一般的樹結
構,而且我們能夠在它們之間做“一致化”(UNIFICATION )。為了要自動化產生這
種結構,我們提出一個新方法--在電腦上作“數學歸納法”。從而我們定義出一套
實用的高次元重寫系統,它能夠做很多原本完全辦不到的事情,使很多發散的系統變
收斂。
我們的方法事實上不僅適用於重寫系統,這種高次元樹狀結構與數學歸納的方法在定
理證明各個領域中都有實用的價值。事實上我們是在一階邏輯(FIRST ORDER LOGIC
)與高階邏輯(SECOND ORDER LOGIC)間找到一種折 ,能作數學歸納的方法表示。
一階邏輯在作“推演”(DEDUCE)時很方便,但無法作“歸納”(INDUCE),高階邏
輯則太複雜而沒有用處,希望我們的研究能開創一個新方向。

QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top