基本介紹
- 中文名：楊張定理
- 提出者：楊樂與張廣厚
- 提出時間：1990年
- 套用學科：幾何
- 適用領域範圍：自動推理領域
- 兩個主要概念：虧值和奇異方向之間的具體聯繫
1
2、1990年楊路、張景中提出了定理機器證明的數值並行方法，在世界上首次用計算機實現了有嚴密理論依據的幾何定理例證法。方法優點之一是占用記憶體小，至今是唯一可用袖珍計算機證明非平凡幾何定理的方法，也是機器證明中唯一可高度並行的算法。在國外文獻中稱此法為“楊張定理”。用此法發現的新定理引起國外專文討論。
1992年張景中等提出了幾何定理可讀證明自動生成的理論、算法和方法，並實現為通用的微機程式。用此新方法已經證明近千個非平凡的幾何定理，其中有幾十個非歐幾何的新定理，對多數定理計算機自動生成了簡捷優美的證明。國外著名計算機科學家在公開發表的出版物中稱這一工作是使計算機能像處理算術那樣處理幾何的發展道路上的里程碑，是自動推理領域三十年來最重要的工作。以此成果為主的項目獲中國科學院 1995 年自然科學一等獎，1997年國家自然科學二等獎。
楊樂、張廣厚在函式值分布論研究中關於"虧值"與"奇異方向"間的具體聯繫的研究成果，還被國際上譽稱為"楊張定理"。80年代，這兩位青年數學家多次應邀赴歐美國家講學，為祖國贏得了榮譽。
