法的推論をMGTP上で実現するには、まず法令文をMGTPの節形式に変換しなくて はならないが、その際、古典的否定と失敗による否定が必要となる。後者を実 現する手法としてKオペレータを用いた節変換方式が提案されていおり、今回 このKオペレータを含む推論機構をMGTPに導入した。
また、様々な試行錯誤の末、得られる機械的な証明には、多くの場合、結論を 得るのには無関係で冗長な推論が含まれている。法的推論のように、結論の説 明が求められる場合には、冗長性を含んだ推論過程よりは、冗長性を排除した 推論過程を提示する方が、利用者には有用である。
そこで、MGTPが出力した証明木から冗長な推論を削除する簡約化の方法を検討 した。それには、推論の依存関係を計算する機構をMGTPに組み込む必要があり、 その実装法を考案した。TPTP問題ライブラリから選択した約300題の例題の内、 9割近い問題で簡約化効果を確認した。