定理の自動証明は公理から出発して定理が導けるまで動作を続けるか、
定理から証明に必要な公理を導き出す。