HOL Light の証明での推論

関数 g で始まる HOL Light の対話的証明作成では，論理式

　~(A0) ∨ … ∨ ~(An) ∨ B

が定理式であること，つまり

　　　　　　　　　　　　　　[A0]
　　　　　　　　　　　　　　 …
　　　　　　　　　　　　　　[An]
　A0,..,An |- B　あるいは　　B

を

　0 [A0]
　………
　n [An]
B

と表示します．

・HOL Light のプルーフマネージャーは証明を遡って作成しますので，結論 B での
　論理記号の消去には導入の推論（R*I），
　論理記号の導入には消去の推論（R*E）
を用います．一方，仮定の列 A0,..,An については

　..,A,.. |- A'　..,A',.. |- B
　−−−−−−−−−−−−−−−−−
　　　 　　..,A,.. |- B

に基づき，..,A,.. |- B から..,A',.. |- Bに遡るために..,A,.. |- A'を準備するのですが，その準備は

　..,A,.. |- A
　−−−−−−
　..,A,.. |- A'

に他なりませんから
　論理記号の消去には仮定を変えないような結論側の消去の推論（R*E），
　論理記号の導入には仮定を変えないような結論側の導入の推論（R*I）
を用います．