張楊定理

1992年張景中等提出了幾何定理可讀證明自動生成的理論、算法和方法，並實現為通用的微機程式。用此新方法已經證明近千個非平凡的幾何定理，其中有幾十個非歐幾何的新定理，對多數定理計算機自動生成了簡捷優美的證明。國外著名計算機科學家在公開發表的出版物中稱這一工作是使計算機能像處理算術那樣處理幾何的發展道路上的里程碑，是自動推理領域三十年來最重要的工作。以此成果為主的項目獲中國科學院 1995 年自然科學一等獎，1997年國家自然科學二等獎。

基本介紹

• 中文名：張楊定理
• 發現時間：1992年
• 提出者：張廣厚與楊樂
• 釋義：發現分布論中的兩個概念的聯繫

名稱來源

我國數學家張廣厚與楊樂合作，首次發現函式值分布論中的兩個主要概念“虧值”和“奇異方向”之間的具體聯繫，被數學界定名為“張楊定理”。

張廣厚

定理影響

1990年張景中、楊路提出了定理機器證明的數值並行方法，在世界上首次用計算機實現了有嚴密理論依據的幾何定理例證法。方法優點之一是占用記憶體小，至今是唯一可用袖珍計算機證明非平凡幾何定理的方法，也是機器證明中唯一可高度並行的算法。在國外文獻中稱此法為“張楊定理”。用此法發現的新定理引起國外專文討論。