根岑式演繹（Gentzen-style deduction）是2018年公布的計算機科學技術名詞。
基本介紹
- 中文名：根岑式演繹
- 外文名：Gentzen-style deduction
- 所屬學科：計算機科學技術
- 公布時間：2018年
定義,出處,
定義
根岑（Gentzen）於1934年提出的證明論中一族用於形式證明的系統，區別於希爾伯特演繹系統，它們對每個聯接或量詞都有簡單明了的推理規則。
出處
《計算機科學技術名詞 》第三版。
根岑式演繹
相關詞條
- 根岑式演繹
根岑式演繹（Gentzen-style deduction）是2018年公布的計算機科學技術名詞。定義根岑（Gentzen）於1934年提出的證明論中一族用於形式證明的系統，區別於希爾伯特演繹系統，它們對每個聯接或量詞都...
- 格哈德·根岑
格哈德·根岑（Gerhard Karl Erich Gentzen），德國的數學家和邏輯學家。簡介 生於德國的Greifswald，由於效力納粹而被逮捕之後，餓死於古拉格附近的戰俘營中。他在1929年到1933年期間是 Hermann Weyl 在哥廷根大學的學生之一。他的主要工作是數學基礎中的證明論，特別是自然演繹和相繼式演算。他的切消定理是證明論語義...
- 自然演繹(數理邏輯)
現代形式的自然演繹是由德國數學家格哈德·根岑於1935年在一篇提交給哥廷根大學數學系的學位論文中獨立提出的。術語自然演繹就是在那篇論文中出現的:首先我希望構造儘可能緊密於實際推理的一種形式化主義。所以提議了“自然演繹演算”。— Gentzen, 《Untersuchungen über das logische Schließen》(Mathematische ...
- 系統化證明方法
這兩種系統都有專門的名稱，嚴格地說，基於公理進行推理推演、並具有句法要求的證明系統是形式公理系統，簡稱形式系統，大致上稱之為“希爾伯特風格的證明”系統；而僅僅基於句法規則進行轉換的證明系統即自然演繹系統，大致上稱之為“根岑風格的證明”系統(“希爾伯特風格”和“根岑風格”還有其他區別，但核心的區別在於此...
- 數理邏輯史
此後不久G.根岑(1909～1945)於1936年就用超窮歸納法證明純粹數論的一致性。這已經不是嚴格意義的有窮方法了。哥德爾定理和過渡時期 希爾伯特方案反映了30年代前數學基礎的爭議，目的是用有窮方法研究包括邏輯和古典數學的形式系統的元邏輯性質，特別是一致性問題。在1928～1936年內主要通過哥德爾的工作，正面或反面地...
- 結構證明論
《結構證明論》是2019年科學出版社出版的圖書，作者是馬明輝。內容簡介 結構證明論研究形式系統中證明的結構.《結構證明論》介紹經典邏輯和直覺主義邏輯的自然演繹和矢列演算,它們是結構證明論的基礎理論.根岑式矢列演算的基本定理是切割消除. 運用證明論研究方法, 通過分析證明的結構可以得到一些邏輯性質,如子公式性質...
- 柯里-霍華德同構
由Gerhard Gentzen介入為研究自然演繹的工具。它已經變成構造邏輯推導的非常有用的演算。它的名字得來自德語的Logischer Kalkül，意思是"邏輯演算"。相繼式演算是關於這個主題的很多研究所選擇的方法。證明邏輯定理的更加直覺的方式是根岑的相繼式演算。相繼式演算以同希爾伯特式證明對應於組合子表達式一樣的方式對應於λ...
- 截消證明方法
在一個根岑風格的推導（樹結構）中，公式具有級(Grade或者Degree)。一種方法是把級數直接表示在樹上作為樹的一個節點以增加直觀性。常用數學證明方法 (1)關係運算證明方法；(2)三段論證明方法；(3)數學歸納法；(4)反證法；(5)構造性證明方法；(6)同態證明方法；(7)解釋性證明方法；(8)系統化證明方法；(9)...
- 非歸結定理證明
著名的根岑系統便是20世紀30年代提出的典型的自然演繹系統。自然演繹系統的顯著特點是在證題全過程中，始終維持前提和結論的明確界限。例如在下例的推理圖式中，橫線以上的H1、H2、H3是前提。橫線以下的C1，C2則是有待證明的結論。由H1，H2可推出C1（根據充分條件的假言推理原則），又根據H3和已推出的C1可推出C2。
- 切消定理
切消定理是確立相繼式演算重要性的主要結果。它最初由格哈德·根岑在他的劃時代論文《邏輯演繹研究》對分別形式化直覺邏輯和經典邏輯的系統LJ和LK做的證明。切消定理聲稱在相繼式演算中，擁有利用了切規則的證明的任何判斷，也擁有無切證明，就是說，不利用切規則的證明。切消定理簡介 相繼式是與多個句子有關的邏輯...
- 漢語照應省略的類型邏輯研究
第三節根岑表述 一、根岑表述 二、可判定性 三、公理表述與根岑表述等價 四、根岑表述的結構規則 五、根岑表述與自然語言推演 第四節ND表述 一、ND表述 二、配以語義的ND表述 第五節加標樹模式表述 一、加標與樹模式 二、加標樹模式的演繹圖示 第六節小結 第三章TLG與非連續現象 第一節關注非連續現象 第...
- 證明方法與理論
9.2 亞里士多德的三段論自然演繹系統和形式系統86 9.3 量化擴展的三段論自然推理系統91 9.4 弗雷格的形式系統F96 9.5 羅素的形式系統R100 9.6 希爾伯特公理系統H105 9.7 根岑的自然演繹系統G與截消證明方法106 9.8 算術形式系統舉例113 9.9 幾何證明公理系統舉例119 參考文獻122 第10章 歸結證明方法...
- 證明論
但1936年，G.根岑降低了希爾伯特的要求，允許使用無窮長的證明，證明了算術公理系統的無矛盾性。到1960年，數學分析的一些片斷的無矛盾性也被證明。20世紀60年代以後，證明論不再局限於無矛盾性的證明。數學證明中的結構，證明的複雜性，數學中不可判定問題都成為證明論的研究課題，1977年，J.帕里斯發現算術理論中的...
- 邏輯和諧
邏輯和諧，由 Michael Dummett 命名，是對可以用於給定的邏輯系統的推理規則的假定約束。具體介紹 邏輯學家格哈德·根岑提議了邏輯連結詞的意義可以用把它們介入到論述中的規則給出。例如，如果你相信“天是藍的”並且還相信“草是綠的”，則你可以如下這樣介入邏輯連線詞“與”: “天是藍的 AND 草是綠的”。Gent...
- 希爾伯特計畫
1936年G.根岑用超限歸納法證明了純數論的協調性，但這已不是希爾伯特原來的計畫。希爾伯特的計畫雖然未能實現，但它對現代數學的發展有很大貢獻。① 它創立了元數學（證明論），在使用了公理化方法和形式化方法以後，它第一次使一門數學理論整體地作為一個確定的、可用數學方法來研究的研究對象；它使得用來說明古典...
