Automated Proof Search

点击翻译按钮获取中文摘要

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.