前回述べたように，HOL Lightでは，goalの集まりであるgoalstackを用いて対話的に証明が作成できます．具体的には，*_TAC の名前を持つ，tactic（戦略関数) を，必要に応じてやり直し・訂正を加えながら，goalstackに段階的に適用することで，その中にある自…

HOL Lightでは，CONJやMPといった推論規則を順次適用する証明作成も原理的には可能ですが，得られる中間結果の授受は少し退屈です．これに対して，証明したい論理式termをgoalとして，それを展開してより簡単なsubgoalsの証明に帰する，下から上への証明作成…