生成規則 generation： 前提（既存証明オブジェクト）がないところから証明オブジェクトを1個作る 変形規則 deformation： 1つの前提から証明オブジェクトを1個作る 組み合わせ規則 combination： 複数の前提から証明オブジェクトを1個作る また、リーズニン…

どうにもならないなーー(溜め息)「除去規則の適用」のレゾリューションアルゴリズムの圏的意味論を考えてみたが、これは複雑。なのに、Isabelleのなかでは天下り。これでは納得出来るわけがない！それはそうと、ポールソンは、メインゴールとサブゴールズと…