本論文では、非自明で論理的に有効な定理を系統的に生成するための厳密な理論的体系が欠如している問題に対処します。新たな自動定理生成理論とツールを提案し、特に矩形標準矛盾と呼ばれる新しい論理構造を定義・証明します。この構造の中心に据えた完全な自動定理生成（ATG）理論が展開され、矩形標準矛盾の二つの主要な性質、すなわち、標準矛盾であることと冗長性がないことが論じられます。これに基づき、矩形標準矛盾を前提部分集合$A$とその補集合の否定$H$に分割することにより、有効な定理$A herefore eg H$が形成されることを証明します。さらに、この理論を実装するために効率的なテンプレートベースのATGアルゴリズムが設計され、矩形自動定理生成器が開発されました。これにより、機械が「検証者」から「発見者」への移行を可能にし、論理および人工知能分野の基礎研究に新たな道を開きます。