Python中逻辑表达式重写规则的设计实现问询

一、规则命名的必要性 #

必须给每个重写规则赋予直观的名称，这是让用户精准选择规则、避免操作歧义的核心前提。针对你列出的规则，推荐命名如下：

• double_negation_intro：A → ¬¬A
• triple_negation：¬A ↔ ¬¬¬A
• demorgan_or：¬(A ∨ B) ↔ ¬A ∧ ¬B
• demorgan_and：¬(A ∧ B) ↔ (A → ¬B) ↔ (B → ¬A)
• double_negation_implication：¬¬(A → B) ↔ (¬¬A → ¬¬B) ↔ (A → ¬¬B) ↔ ¬¬(¬A ∨ B)
• implication_to_or_negation：¬(A → B) ↔ ¬(¬A ∨ B)
• contrapositive：(A → B) ↔ (¬B → ¬A)

二、多等价形式的处理策略 #

对于包含多个等价分支的规则，比如¬(A ∧ B) ↔ (A → ¬B) ↔ (B → ¬A)，可以采用两种实用方案：

1. 拆分双向子规则：把一条多等价规则拆分为若干独立的双向转换对，比如：
   • demorgan_and_to_left_implies：¬(A ∧ B) ↔ (A → ¬B)
   • demorgan_and_to_right_implies：¬(A ∧ B) ↔ (B → ¬A)
   • implies_left_to_right：(A → ¬B) ↔ (B → ¬A)
2. 参数化目标形式：在规则函数中加入参数，让用户指定转换的目标等价分支。比如调用apply_rule(expr, "demorgan_and", target="left_implies")直接得到(A→¬B)。

三、规则的表示与实现示例 #

基于你现有的表达式类，采用模式匹配+替换的方式实现重写规则：每个规则函数先检查输入表达式的结构是否匹配规则模式，匹配则返回转换后的表达式，否则返回原表达式。

核心实现代码 #

在现有代码基础上添加重写规则模块：

# 重写规则实现
def apply_double_negation_intro(expr):
    """A → ¬¬A"""
    return Not(Not(expr))

def apply_triple_negation(expr, direction="to_triple"):
    """¬A ↔ ¬¬¬A
    direction可选值: "to_triple" (¬A → ¬¬¬A), "from_triple" (¬¬¬A → ¬A)
    """
    if direction == "to_triple" and isinstance(expr, Not):
        return Not(Not(expr))
    elif direction == "from_triple" and isinstance(expr, Not) and isinstance(expr.operand, Not) and isinstance(expr.operand.operand, Not):
        return expr.operand.operand
    return expr

def apply_demorgan_or(expr, direction="to_and"):
    """¬(A ∨ B) ↔ ¬A ∧ ¬B
    direction可选值: "to_and" (¬(A∨B)→¬A∧¬B), "to_or" (¬A∧¬B→¬(A∨B))
    """
    if direction == "to_and" and isinstance(expr, Not) and isinstance(expr.operand, Or):
        a = expr.operand.LHS
        b = expr.operand.RHS
        return And(Not(a), Not(b))
    elif direction == "to_or" and isinstance(expr, And) and isinstance(expr.LHS, Not) and isinstance(expr.RHS, Not):
        a = expr.LHS.operand
        b = expr.RHS.operand
        return Not(Or(a, b))
    return expr

def apply_contrapositive(expr, direction="to_contrapositive"):
    """(A → B) ↔ (¬B → ¬A)
    direction可选值: "to_contrapositive" (A→B→¬B→¬A), "from_contrapositive" (¬B→¬A→A→B)
    """
    if direction == "to_contrapositive" and isinstance(expr, Implies):
        a = expr.LHS
        b = expr.RHS
        return Implies(Not(b), Not(a))
    elif direction == "from_contrapositive" and isinstance(expr, Implies) and isinstance(expr.LHS, Not) and isinstance(expr.RHS, Not):
        b = expr.LHS.operand
        a = expr.RHS.operand
        return Implies(a, b)
    return expr

# 多等价规则的参数化实现
def apply_demorgan_and(expr, target="implies_left"):
    """¬(A ∧ B) ↔ (A → ¬B) ↔ (B → ¬A)
    target可选值: "implies_left" (转成A→¬B), "implies_right" (转成B→¬A), "from_implies_left" (从A→¬B转回¬(A∧B)), "from_implies_right" (从B→¬A转回¬(A∧B))
    """
    # 从¬(A∧B)转成目标形式
    if isinstance(expr, Not) and isinstance(expr.operand, And):
        a = expr.operand.LHS
        b = expr.operand.RHS
        if target == "implies_left":
            return Implies(a, Not(b))
        elif target == "implies_right":
            return Implies(b, Not(a))
    # 从(A→¬B)转回¬(A∧B)
    elif target == "from_implies_left" and isinstance(expr, Implies) and isinstance(expr.RHS, Not):
        a = expr.LHS
        b = expr.RHS.operand
        return Not(And(a, b))
    # 从(B→¬A)转回¬(A∧B)
    elif target == "from_implies_right" and isinstance(expr, Implies) and isinstance(expr.RHS, Not):
        b = expr.LHS
        a = expr.RHS.operand
        return Not(And(a, b))
    return expr

使用示例 #

# 创建测试表达式
A = Variable("A")
B = Variable("B")
expr1 = Not(Or(A, B))
# 应用德摩根律（或的否定转合取）
result1 = apply_demorgan_or(expr1)
print(result1)  # 输出: ¬A ∧ ¬B

expr2 = Implies(A, B)
# 应用逆否命题规则
result2 = apply_contrapositive(expr2)
print(result2)  # 输出: ¬B → ¬A

expr3 = Not(And(A, B))
# 转成A→¬B
result3 = apply_demorgan_and(expr3, target="implies_left")
print(result3)  # 输出: A → ¬B

四、扩展建议 #

1. 递归应用规则：实现递归遍历表达式树，对所有符合模式的子表达式自动应用规则；
2. 规则组合：支持用户组合多个规则，比如先应用逆否命题再应用双重否定；
3. 模式匹配优化：使用matchpy等库简化规则的模式定义，减少重复的类型判断代码。

内容的提问来源于stack exchange，提问作者Jasper