Automated Proof Search

本研究的目标是开发启发式动机程序，可以有效地找到逻辑定理的可理解和自然的证明。这种自动证明搜索的挑战是将基于人和逻辑的方法结合起来进行定理证明。预计自动证明搜索将导致发现包含人类论证的重要结构的程序，从而可以用于构建“智能”导师。卡内基梅隆证明导师（CPT）依赖于这样一个经典句子逻辑的搜索过程——以一种计算和教学上有效的方式。本研究将以CPT的经验为基础，将其理论基础——插补演算、完备性定理和范式定理——扩展到直觉式句子逻辑和谓词逻辑。这个理论基础是至关重要的：它不仅建立了问题空间，并为证明搜索提供了一些（尽管是最小的）指导，而且还保证了证明过程的正确性。研究任务包括：通过嵌入演算统一处理经典和非经典句子逻辑；将句子逻辑中的证明搜索推广到谓词逻辑并将方法从纯逻辑扩展到集合论。

The goal of this research is to develop heuristically motivated procedures that can find intelligible and natural proofs of logical theorems efficiently. The challenge in such automated proof search is to join human and logic based approaches to theorem proving. Automated proof search is expected to lead to the discovery of procedures that incorporate significant structures of human argumentation and can thus be exploited for building "intelligent" tutors. The Carnegie Mellon Proof Tutor (CPT) depends on such a search procedure for classical sentential logic -- in a computational and pedagogically efficient way. The research will build on the experience with CPT and the extension of its theoretical base, the Intercalation Calculus together with completeness and normal form theorems, to intuitionistic sentential logic and to predicate logic. This theoretical base is crucial: it not only sets up the problem space and provides some, albeit minimal guidance for proof search, but it also guarantees the correctness of proof procedures. Research tasks include: treating classical and non-classical sentential logics in a uniform way through intercalation calculi; generalizing proof search in sentential logics to predicate logic; and extending the approach beyond pure logic to set theory.