>>54
それは違う。
論理的帰結としてrequireになることがわかった枝をこのschemeの論理プログラムでは自動的に修正できない。
そこで、プログラマーが自分でその枝をrequireにしてやらなければならない。
半自動定理証明を調べてみろ。