P53 - 归结原理

2026-09-07 00:00    #Haskell   #99题   #逻辑  

P53 - 归结原理

Resolution rule for theorem proving

官方模块：Problems.P53　核心函数：isTheorem

← P52 合取范式 | P54 二叉树定义 →

题目描述

用归结原理判断一组公理能否推出一个结论。即将 A∧¬CA \land \neg C 转为 CNF，反复应用归结规则直到推出空子句（矛盾）或无法继续。

数据类型与原理

1import qualified Data.Set as Set
2
3type Clause = Set.Set Formula

要证明公理集合 AA 蕴含结论 CC，把 A∧¬CA\land\neg C 转成 CNF，然后尝试推出空子句。若推出矛盾，原命题成立。

函数签名

1isTheorem :: [Formula] -> Formula -> Bool

实现

方法一：标准归结算法

 1isTheorem :: [Formula] -> Formula -> Bool
 2isTheorem axioms conjecture = refute initial
 3  where
 4    Conjoin clauses = toConjunctiveNormalForm
 5      (Conjoin (Complement conjecture : axioms))
 6    initial = Set.fromList [Set.fromList (disjuncts c) | c <- clauses]
 7
 8    disjuncts (Disjoin fs) = fs
 9    disjuncts f            = [f]
10
11    refute clauses
12      | Set.member Set.empty clauses = True
13      | Set.null new                  = False
14      | otherwise                     = refute (Set.union clauses new)
15      where
16        pairs = [(c1, c2) | c1 <- Set.toList clauses, c2 <- Set.toList clauses, c1 < c2]
17        generated = Set.fromList
18          [ resolvent
19          | (c1, c2) <- pairs
20          , resolvent <- resolve c1 c2
21          , not (tautology resolvent)
22          ]
23        new = generated `Set.difference` clauses
24
25    resolve c1 c2 =
26      [ Set.union (Set.delete literal c1)
27                  (Set.delete (negateLiteral literal) c2)
28      | literal <- Set.toList c1
29      , negateLiteral literal `Set.member` c2
30      ]
31
32    negateLiteral (Complement literal) = literal
33    negateLiteral literal              = Complement literal
34
35    tautology clause = any
36      (\literal -> negateLiteral literal `Set.member` clause)
37      (Set.toList clause)

从 CNF 子句集开始，反复寻找互补文字对并应用归结规则。当空子句出现时，结论得证。

方法二：真值表验证（穷举法）

1isTheorem :: [Formula] -> Formula -> Bool
2isTheorem axioms conjecture =
3  all valid (environments (variables (Conjoin (conjecture : axioms))))
4  where
5    valid env = evaluate env (Conjoin axioms) `implies` evaluate env conjecture
6    implies a b = not a || b

对所有可能的环境（真值赋值），检查公理成立时结论是否也成立。本质上做了一次穷举验证——变量数少时可用，变量多时组合爆炸。

方法对比

方法特点适用场景
归结原理符号推导，可处理大变量集标准做法
真值表穷举枚举所有环境变量很少（<10）时验证用

测试

1>>> let p = Variable "p"; q = Variable "q"
2>>> isTheorem [Disjoin [Complement p, q], Disjoin [Complement q, p]] (Disjoin [Complement p, Complement (Complement p)])
3True
4>>> isTheorem [p] q
5False

参考