一阶谓词逻辑标准化分离

### 一阶谓词逻辑标准化分离

在一阶谓词逻辑中，标准化分离是指将复杂的公式转换成标准形式的过程。这一过程有助于简化公式的结构，使其更容易处理和分析。

#### 定义与目标
标准化分离的目标是通过一系列变换，使得任何给定的一阶谓词逻辑公式能够被转化为一个特定的标准形式。这种标准形式通常指的是前束范式（Prenex Normal Form, PNF），其中所有的量词都位于最左边，并且整个公式由这些量词后面跟着一个无量词的矩阵组成[^1]。

#### 变换步骤
为了实现上述目标，需要遵循以下几个主要步骤：

- **消除蕴含符**：首先替换掉所有出现的蕴涵符号 (→)，因为这可以通过等价变形来完成，即 \( A \rightarrow B \) 等同于 \( \neg A \vee B \)。

- **移动否定运算符至原子层**：接着应用德·摩根定律和其他双重否定律，直到所有的否定操作只作用于单个命题变元或常数之上。

- **引入新变量以去除存在量化器下的合取项**：当遇到形如 \( (\exists x)(A(x)\wedge B(y)) \) 的情况时，应该创建一个新的变量 z 来代替 y 并保持其他部分不变；这样做是为了确保每个存在量化的子句内部不含有多重约束条件。

- **分配析取到合取之上**：最后一步是对含有多个析取项的表达式执行斯科伦化（Skolemization）。这意味着对于每一个普遍性的陈述，我们都会找到相应的实例化版本，从而消除了剩余的存在量词。

def standardize_separation(formula):
    # Step 1: Eliminate implication symbols
    formula = eliminate_implications(formula)

    # Step 2: Move negation operators inward using De Morgan's laws and double-negation elimination
    formula = move_negations_inward(formula)

    # Step 3: Remove existential quantifiers from conjunctions by introducing new variables
    formula = remove_existential_quantifiers_from_conjunctions(formula)

    # Step 4: Distribute disjunction over conjunction to achieve prenex normal form
    standardized_formula = distribute_disjunction_over_conjunction(formula)
    
    return standardized_formula