代数の公理系を満たす有限モデルの導出アルゴリ ズムの改良