《證明等式的計算機輔助教學系統》是依託清華大學，由李大法擔任項目負責人的面上項目。
基本介紹
- 中文名：證明等式的計算機輔助教學系統
- 依託單位：清華大學
- 項目負責人：李大法
- 項目類別：面上項目
- 批准號：69673032
- 申請代碼：F0209
- 研究期限：1997-01-01 至 1999-12-31
- 負責人職稱：教授
- 支持經費：10（萬元）
項目摘要
本課題是證明等式的計算機輔助教學系統。它涉及的內容是怎樣的在計算機上證明等式，怎樣用於教學，理論上我們得到如下結果：①我們提出01-paramodulation。給等式t=s和r=h，對項t和t的自變數位置上的項做等式替換，對更深入子項不做替換，我們證明了它是完備的，②證明等式需要反身性、對稱性和遞性作為公理。使用我們的定理證明器發現用兩個公理可代替上述三公理，③雖然禁止Paramodulation into variables是完備的，我們指出這對Input paramodulation是不完備的，當變數在一個等式中只出現一次時，我們證明在input paramodulation中禁止Paramodulation into variasles是完備的。我們做了三個軟體系統，①受限制的Input paramodulation②受限制Unitparamodulation③01-paramodulation。打算將上述系統用於網路教學。
