- 命題の真偽判定： 白黒つける、決着をつける。どうやって？
- 証明項の正当性検証： 構文を決めれば機械的に決定出来るか、または無限走行
- 証明項の生成工程〈リーズニングプロセス〉の正当性検証： 構文を決めれば機械的に決定出来るか、または無限走行
証明項の正当性検証が型チェックエンジンがやること。証明項の生成工程の正当性検証が対話的支援系やスクリプトチェッカーがやること。
証明項の正当性検証が型チェックエンジンがやること。証明項の生成工程の正当性検証が対話的支援系やスクリプトチェッカーがやること。