自動定理発見問題を解決するために強相関論理に基づく前向き推論を用いた自動定理発見法（以下、SRATF）が提案され、その有用性が理論的に示された。しかし、SRATFの有用性を実証的に示すためにはSRATFの改善が必要である。SRATFでは論理結合子の入れ子の度合いを制限することにより前向き推論で扱う論理式の数を制限している。入れ子の度合いの制限の厳しさと実行時間はトレードオフとなっている。本研究では演繹定理を用いて強相関論理の論理定理を推論規則化することで、入れ子の度合いの制限を厳しいままで、前向き推論においてより多くの論理式を扱えるようにした。