#自动定理生成

三角标准矛盾构造法：一阶逻辑定理生成免证明即正确

论文提出基于三角标准矛盾的一阶逻辑自动定理生成（ATG）构造框架：从选定文字构造极小不可满足子句集，保留部分子句为前提、取某子句或子句合取之否定为结论，从而由构造保证定理正确，无需逐例证明。作者在 Δ1 基础上提出 Δ2–Δ8 共七种方法，形成八法统一家族，其中 Δ1–Δ4 已实现并发布。