MyProver

一个用于学习 Haskell 的命题逻辑自然演绎证明器。

功能

• 解析命题逻辑公式（支持 Unicode 与 ASCII 两种语法）。
• 提供将公式归约为 →⊥ 范式的辅助工具。
• 自动搜索自然演绎证明树。
• 支持用户自定义上下文（假设集）。
• 对生成的证明树进行独立检查。

输入语法

变量名：A, B, P1, foo_bar, ...

Unicode：→  ∧  ∨  ¬  ⊥
ASCII：  -> && || ! ~ bot _|_ false

括号： ( )

示例：

P -> P
P -> (Q -> P)
P && Q -> Q && P
!P -> bot

REPL 使用

请输入假设（逗号分隔，直接回车表示空）：P, P -> Q
当前上下文：P, P -> Q
请输入待证目标：Q

程序会尝试自动构造证明，并调用检查器验证其正确性。

构建与运行

用 Cabal

cabal build
cabal run myprover
cabal test

项目结构

app/Main.hs          REPL / 交互入口
src/Types.hs         数据类型定义
src/Parser.hs        词法分析与语法分析
src/Normalizer.hs    公式归约（→⊥ 范式）
src/Pretty.hs        美化输出
src/Prover.hs        证明搜索
src/Checker.hs       证明检查器
test/Spec.hs         手动测试集合

已实现的规则

• → 引入 / 消除
• ∧ 引入 / 左消除 / 右消除
• ∨ 左引入 / 右引入 / 消除
• ¬ 引入 / 消除
• ⊥ 引入 / 消除

已知限制

• 证明器采用深度受限的回溯搜索，复杂命题可能失败或超限。