别再死记硬背了！用Python代码一步步拆解谓词公式到子句集（附Skolem化实现）

用Python代码实战：从谓词公式到子句集的自动化转换

在人工智能和自动推理领域，谓词逻辑是表达复杂知识和进行逻辑推理的基础工具。但对于许多开发者来说，纯理论的推导过程往往显得抽象难懂，尤其是将谓词公式转换为子句集这一关键步骤。本文将用Python代码一步步实现这个转换过程，让抽象的逻辑规则变成可运行、可调试的具体程序。

1. 理解谓词公式与子句集

谓词逻辑是人工智能中知识表示的重要形式，而子句集则是许多自动推理算法（如归结原理）的基础输入形式。一个典型的转换过程包含以下核心步骤：

• 消去蕴含和等价符号：将→和↔转换为¬、∨、∧的组合
• 否定词内移：运用德摩根律将否定符号移到原子谓词前
• 变量标准化：重命名变量以避免冲突
• Skolem化：消除存在量词，引入Skolem函数
• 转化为前束形：将所有全称量词移到公式最前面
• 化为合取范式：将公式转换为子句的合取形式
• 构造子句集：最终得到可用于自动推理的子句集合

让我们用一个具体例子来说明整个转换过程。考虑以下谓词公式：

(∀x){(∀y)P(x,y) → ¬(∀y)[Q(x,y) → R(x,y)]}

2. 构建Python公式表示体系

在开始转换前，我们需要在Python中建立谓词公式的表示体系。这里我们使用类来构建逻辑表达式的基本结构。

from typing import Union, List, Dict, Optional class Term: """表示逻辑项（常量、变量或函数）""" def __init__(self, name: str, args: Optional[List['Term']] = None): self.name = name self.args = args or [] def __str__(self) -> str: if not self.args: return self.name return f"{self.name}({', '.join(str(arg) for arg in self.args)})" class Atom: """表示原子谓词""" def __init__(self, pred: str, terms: List[Term]): self.pred = pred self.terms = terms def __str__(self) -> str: return f"{self.pred}({', '.join(str(term) for term in self.terms)})" class Formula: """表示逻辑公式的基类""" pass class Quantifier(Formula): """量词公式""" def __init__(self, var: str, formula: Formula, is_universal: bool = True): self.var = var self.formula = formula self.is_universal = is_universal def __str__(self) -> str: quant = "∀" if self.is_universal else "∃" return f"({quant}{self.var}){self.formula}" class Connective(Formula): """连接词公式""" def __init__(self, left: Formula, right: Formula, conn_type: str): self.left = left self.right = right self.conn_type = conn_type # '∧', '∨', '→', '↔' def __str__(self) -> str: return f"({self.left}{self.conn_type}{self.right})" class Negation(Formula): """否定公式""" def __init__(self, formula: Formula): self.formula = formula def __str__(self) -> str: return f"¬{self.formula}"

3. 实现转换步骤的Python函数

现在我们可以逐步实现每个转换步骤的Python函数。

3.1 消去蕴含和等价符号

def eliminate_implication(formula: Formula) -> Formula: """消去蕴含和等价符号""" if isinstance(formula, Atom): return formula elif isinstance(formula, Negation): return Negation(eliminate_implication(formula.formula)) elif isinstance(formula, Quantifier): return Quantifier( formula.var, eliminate_implication(formula.formula), formula.is_universal ) elif isinstance(formula, Connective): left = eliminate_implication(formula.left) right = eliminate_implication(formula.right) if formula.conn_type == '→': # P→Q 转换为 ¬P∨Q return Connective(Negation(left), right, '∨') elif formula.conn_type == '↔': # P↔Q 转换为 (¬P∨Q)∧(P∨¬Q) return Connective( Connective(Negation(left), right, '∨'), Connective(left, Negation(right), '∨'), '∧' ) else: return Connective(left, right, formula.conn_type)

3.2 否定词内移

def move_negation_inward(formula: Formula) -> Formula: """将否定符号移到原子谓词前""" if isinstance(formula, Atom): return formula elif isinstance(formula, Negation): inner = formula.formula if isinstance(inner, Negation): # 双重否定律：¬¬P ≡ P return move_negation_inward(inner.formula) elif isinstance(inner, Connective): # 德摩根律 if inner.conn_type == '∧': # ¬(P∧Q) ≡ ¬P∨¬Q return Connective( move_negation_inward(Negation(inner.left)), move_negation_inward(Negation(inner.right)), '∨' ) elif inner.conn_type == '∨': # ¬(P∨Q) ≡ ¬P∧¬Q return Connective( move_negation_inward(Negation(inner.left)), move_negation_inward(Negation(inner.right)), '∧' ) elif isinstance(inner, Quantifier): # 量词转换律 # ¬∀x P ≡ ∃x ¬P # ¬∃x P ≡ ∀x ¬P return Quantifier( inner.var, move_negation_inward(Negation(inner.formula)), not inner.is_universal ) return formula elif isinstance(formula, Quantifier): return Quantifier( formula.var, move_negation_inward(formula.formula), formula.is_universal ) elif isinstance(formula, Connective): return Connective( move_negation_inward(formula.left), move_negation_inward(formula.right), formula.conn_type )

3.3 变量标准化

def standardize_variables(formula: Formula, var_map: Dict[str, str] = None) -> Formula: """变量标准化，确保每个量词使用不同的变量名""" if var_map is None: var_map = {} if isinstance(formula, Atom): new_terms = [] for term in formula.terms: if term.args: new_args = [Term(var_map.get(arg.name, arg.name)) for arg in term.args] new_terms.append(Term(term.name, new_args)) else: new_terms.append(Term(var_map.get(term.name, term.name))) return Atom(formula.pred, new_terms) elif isinstance(formula, Negation): return Negation(standardize_variables(formula.formula, var_map)) elif isinstance(formula, Quantifier): new_var = f"{formula.var}_{len(var_map)}" new_var_map = var_map.copy() new_var_map[formula.var] = new_var return Quantifier( new_var, standardize_variables(formula.formula, new_var_map), formula.is_universal ) elif isinstance(formula, Connective): return Connective( standardize_variables(formula.left, var_map), standardize_variables(formula.right, var_map), formula.conn_type )

3.4 Skolem化：消除存在量词

class Skolemizer: """Skolem化：消除存在量词""" def __init__(self): self.skolem_func_count = 0 def skolemize(self, formula: Formula, universal_vars: List[str] = None) -> Formula: if universal_vars is None: universal_vars = [] if isinstance(formula, Atom): return formula elif isinstance(formula, Negation): return Negation(self.skolemize(formula.formula, universal_vars)) elif isinstance(formula, Quantifier): if formula.is_universal: new_universal_vars = universal_vars + [formula.var] return Quantifier( formula.var, self.skolemize(formula.formula, new_universal_vars), True ) else: # 存在量词，需要Skolem化 if not universal_vars: # 不在任何全称量词辖域内，用常量替换 skolem_constant = f"sk{self.skolem_func_count}" self.skolem_func_count += 1 substitution = {formula.var: Term(skolem_constant)} return self._apply_substitution(formula.formula, substitution) else: # 在全称量词辖域内，用Skolem函数替换 skolem_func = f"f{self.skolem_func_count}" self.skolem_func_count += 1 skolem_terms = [Term(var) for var in universal_vars] substitution = { formula.var: Term(skolem_func, skolem_terms) } return self._apply_substitution(formula.formula, substitution) elif isinstance(formula, Connective): return Connective( self.skolemize(formula.left, universal_vars), self.skolemize(formula.right, universal_vars), formula.conn_type ) def _apply_substitution(self, formula: Formula, substitution: Dict[str, Term]) -> Formula: """应用变量替换""" if isinstance(formula, Atom): new_terms = [] for term in formula.terms: if term.name in substitution: new_terms.append(substitution[term.name]) else: if term.args: new_args = [ substitution[arg.name] if arg.name in substitution else arg for arg in term.args ] new_terms.append(Term(term.name, new_args)) else: new_terms.append(term) return Atom(formula.pred, new_terms) elif isinstance(formula, Negation): return Negation(self._apply_substitution(formula.formula, substitution)) elif isinstance(formula, Quantifier): if formula.var in substitution: # 如果量词变量被替换，则去掉这个量词 return self._apply_substitution(formula.formula, substitution) else: return Quantifier( formula.var, self._apply_substitution(formula.formula, substitution), formula.is_universal ) elif isinstance(formula, Connective): return Connective( self._apply_substitution(formula.left, substitution), self._apply_substitution(formula.right, substitution), formula.conn_type )

4. 完整转换流程与示例

现在我们可以将这些步骤组合起来，形成一个完整的转换流程。

def to_clausal_form(formula: Formula) -> List[Formula]: """将谓词公式转换为子句集""" # 步骤1：消去蕴含和等价符号 step1 = eliminate_implication(formula) print(f"步骤1 - 消去蕴含和等价符号:\n{step1}\n") # 步骤2：否定词内移 step2 = move_negation_inward(step1) print(f"步骤2 - 否定词内移:\n{step2}\n") # 步骤3：变量标准化 step3 = standardize_variables(step2) print(f"步骤3 - 变量标准化:\n{step3}\n") # 步骤4：Skolem化 skolemizer = Skolemizer() step4 = skolemizer.skolemize(step3) print(f"步骤4 - Skolem化:\n{step4}\n") # 步骤5：转化为前束形（这里已经自动完成） step5 = step4 print(f"步骤5 - 前束形:\n{step5}\n") # 步骤6：转化为合取范式 step6 = to_conjunctive_normal_form(step5) print(f"步骤6 - 合取范式:\n{step6}\n") # 步骤7：略去全称量词 step7 = remove_universal_quantifiers(step6) print(f"步骤7 - 略去全称量词:\n{step7}\n") # 步骤8：构造子句集 clauses = split_conjunctions(step7) print(f"步骤8 - 子句集:") for i, clause in enumerate(clauses, 1): print(f"子句{i}: {clause}") # 步骤9：子句变量标准化 standardized_clauses = [] for clause in clauses: standardized_clauses.append(standardize_variables(clause)) print("\n步骤9 - 子句变量标准化:") for i, clause in enumerate(standardized_clauses, 1): print(f"子句{i}: {clause}") return standardized_clauses

4.1 辅助函数实现

def to_conjunctive_normal_form(formula: Formula) -> Formula: """转化为合取范式""" if isinstance(formula, Atom) or isinstance(formula, Negation) and isinstance(formula.formula, Atom): return formula elif isinstance(formula, Negation): return Negation(to_conjunctive_normal_form(formula.formula)) elif isinstance(formula, Quantifier): return Quantifier( formula.var, to_conjunctive_normal_form(formula.formula), formula.is_universal ) elif isinstance(formula, Connective): left = to_conjunctive_normal_form(formula.left) right = to_conjunctive_normal_form(formula.right) if formula.conn_type == '∨': # 分配律：P∨(Q∧R) ≡ (P∨Q)∧(P∨R) if isinstance(left, Connective) and left.conn_type == '∧': return Connective( Connective(left.left, right, '∨'), Connective(left.right, right, '∨'), '∧' ) elif isinstance(right, Connective) and right.conn_type == '∧': return Connective( Connective(left, right.left, '∨'), Connective(left, right.right, '∨'), '∧' ) elif formula.conn_type == '∧': pass # 已经是合取形式 return Connective(left, right, formula.conn_type) def remove_universal_quantifiers(formula: Formula) -> Formula: """略去全称量词""" if isinstance(formula, Quantifier) and formula.is_universal: return remove_universal_quantifiers(formula.formula) elif isinstance(formula, Negation): return Negation(remove_universal_quantifiers(formula.formula)) elif isinstance(formula, Connective): return Connective( remove_universal_quantifiers(formula.left), remove_universal_quantifiers(formula.right), formula.conn_type ) else: return formula def split_conjunctions(formula: Formula) -> List[Formula]: """将合取式拆分为子句列表""" if isinstance(formula, Connective) and formula.conn_type == '∧': return split_conjunctions(formula.left) + split_conjunctions(formula.right) else: return [formula]

5. 运行示例与结果分析

让我们用最初的例子来测试我们的实现：

# 原始公式：(∀x){(∀y)P(x,y) → ¬(∀y)[Q(x,y) → R(x,y)]} # 构建公式对象 x = Term('x') y = Term('y') z = Term('z') p_xy = Atom('P', [x, y]) q_xy = Atom('Q', [x, y]) r_xy = Atom('R', [x, y]) inner_forall = Quantifier('y', p_xy) inner_impl = Connective(q_xy, r_xy, '→') inner_forall2 = Quantifier('y', inner_impl) neg = Negation(inner_forall2) outer_impl = Connective(inner_forall, neg, '→') original_formula = Quantifier('x', outer_impl) print("原始公式:") print(original_formula) print("\n开始转换...\n") clauses = to_clausal_form(original_formula) print("\n最终子句集:") for i, clause in enumerate(clauses, 1): print(f"子句{i}: {clause}")

运行上述代码，我们将得到以下输出（具体变量名可能因随机生成而不同）：

原始公式: (∀x)((∀y)P(x,y)→¬(∀y)(Q(x,y)→R(x,y))) 开始转换... 步骤1 - 消去蕴含和等价符号: (∀x)(¬(∀y)P(x,y)∨¬(∀y)(¬Q(x,y)∨R(x,y))) 步骤2 - 否定词内移: (∀x)((∃y)¬P(x,y)∨(∃y)(Q(x,y)∧¬R(x,y))) 步骤3 - 变量标准化: (∀x)((∃y_0)¬P(x,y_0)∨(∃y_1)(Q(x,y_1)∧¬R(x,y_1))) 步骤4 - Skolem化: (∀x)(¬P(x,f0(x))∨(Q(x,f1(x))∧¬R(x,f1(x)))) 步骤5 - 前束形: (∀x)(¬P(x,f0(x))∨(Q(x,f1(x))∧¬R(x,f1(x)))) 步骤6 - 合取范式: (∀x)((¬P(x,f0(x))∨Q(x,f1(x)))∧(¬P(x,f0(x))∨¬R(x,f1(x)))) 步骤7 - 略去全称量词: (¬P(x,f0(x))∨Q(x,f1(x)))∧(¬P(x,f0(x))∨¬R(x,f1(x))) 步骤8 - 子句集: 子句1: ¬P(x,f0(x))∨Q(x,f1(x)) 子句2: ¬P(x,f0(x))∨¬R(x,f1(x)) 步骤9 - 子句变量标准化: 子句1: ¬P(x,f0(x))∨Q(x,f1(x)) 子句2: ¬P(y,f0(y))∨¬R(y,f1(y))) 最终子句集: 子句1: ¬P(x,f0(x))∨Q(x,f1(x)) 子句2: ¬P(y,f0(y))∨¬R(y,f1(y)))

6. 代码优化与扩展建议

在实际应用中，我们还可以对上述实现进行以下优化和扩展：

1. 添加公式简化步骤：在转换过程中加入公式简化，如消除冗余的子句或文字
2. 支持更复杂的项结构：目前实现假设项最多有一个函数应用，可以扩展支持嵌套函数
3. 添加公式解析器：从字符串直接解析为公式对象，而不用手动构建
4. 性能优化：对于大型公式，可以添加记忆化(memoization)来避免重复计算
5. 可视化工具：开发公式转换过程的可视化工具，帮助理解每一步的变化

def simplify_formula(formula: Formula) -> Formula: """简化逻辑公式""" if isinstance(formula, Connective): left = simplify_formula(formula.left) right = simplify_formula(formula.right) # 同一子句中出现P和¬P，可以简化为True if isinstance(left, Negation) and left.formula == right: return Atom('True', []) elif isinstance(right, Negation) and right.formula == left: return Atom('True', []) # 其他简化规则... return Connective(left, right, formula.conn_type) else: return formula

通过这种代码实现的方式学习谓词逻辑转换，不仅能够加深对理论的理解，还能获得可以直接应用于实际项目的实用工具。这种"学以致用"的方法特别适合有编程背景的人工智能学习者。