Automated Theorem Proving

Automated Theorem Proving的目标是在给定一个猜想（目标定理）和已知事实的知识库的情况下，自动生成形式语言表达的证明。该技术在软件和硬件系统的验证与合成等多领域具有重要应用价值。