原始公式
辖域分析
辖域是量词作用的范围,决定了变元的约束关系
变元分类
🔗 约束变元
被量词约束的变元,其值由量词域决定
🔓 自由变元
不受任何量词约束的变元,可自由取值
闭式检测
约束变元换名
约束变元可以重命名而不改变公式的语义,前提是新变元不会产生冲突