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.