量化公式
1.简介
量化允许我们指定谓词的有效性范围, 换句话说, 即谓词应包含的域(值的范围). 用于指定量化的逻辑中使用的语法元素称为量词(quantifier). 最常用的两个量词分别是全称量词 "\(\forall\)"和存在量词 "\(\exists\)". 这两个量词是可以相互转换的: \[ \forall x.\varphi \Longleftrightarrow \neg\exists x.\neg\varphi. \] 一些量化声明的例子:
对于任意整数 \(x\), 存在一个整数 \(y\) 小于 \(x\): \[ \forall x\in \mathbb{Z}.\exists y\in \mathbb{Z}.y\lt x. \]
存在一个整数 \(y\), 对于任意一个整数 \(x\), \(x\) 总是大于 \(y\): \[ \exists y\in\mathbb{Z}.\forall x\in\mathbb{Z}.x\gt y. \]
对于任意大于1的自然数 \(n\), 存在一个质数 \(p\), 使得 \(n\lt p\lt 2n\): \[ \forall n\in\mathbb{N}.\exists p\in\mathbb{N}.n\gt 1\Longrightarrow (isprime(p)\land n\lt p\lt 2n). \]
在以上三个示例中, 全称量词和存在量词之间存在量词交替. 实际上, 我们在前面考虑的可满足性和有效性问题可以解释为具有非交替量词的公式的判定问题. 当我们考虑命题公式 \[ x\lor y \] 是否可满足时, 可以等价地考虑是否 存在 一组 \(x,y\) 的赋值满足该公式. 相似地, 当我们考虑对于 \(x,y\in \mathbb{N}\) \[ x\gt y\lor x\lt y \] 是否成立, 可以等价地考虑对于 任意 自然数 \(x,y\), 该公式是否成立.
所以, 上面两个判定问题地等价形式分别是 \[ \exists x\in \mathbb{B}.\exists y\in\mathbb{B}.(x\lor y) \] 和 \[ \forall x\in\mathbb{N}.\forall y\in\mathbb{N}.x\gt y\lor x\lt y. \] 下面引入两个在量化公式中比较重要的两个概念.
自由变量(free variable). 在一个给定的公式中, 至少有一个变量不受任何量词约束, 那么该变量称作自由变量.
句子(sentence). 如果一个公式 \(\mathcal{Q}\) 中的变量没有一个是自由变量, 那么该公式就成为句子.
我们只考虑句子形式的公式, 也就是说只关注无自由变量公式的判定问题. 应该注意到, 带有量词的任意一阶理论都是不可判定的. 所以我们只讨论可判定的理论.
1.1 量化布尔公式
量化命题逻辑(quantified propositional logic)是用量词增强的命题逻辑. 量化命题逻辑中的句子被称为量化布尔公式(quantified Boolean formulas, QBF). 逻辑允许的句子集合由以下语法定义: \[ \begin{align*} formula&:formula\land formula\ |\ \neg formula\ |\ (formula)\ \\ &\;|\;identifier\ |\ \exists identifier.formula \end{align*} \] QBF 可用于规划问题的建模, 比如说国际象棋问题. 比如说, 对于一个象棋玩家来说, 判断是否存在一个在 \(k\) 步之内取胜的策略. 给定棋盘状态并假设白棋先行, 不管黑棋的步数如何, 白棋能否以 \(k\) 步率先吃掉黑棋的国王. 这类问题可以用QBF进行建模, 因为这相当于问白棋是否 存在 这样一种走法, 使得对于黑棋 所有 可能的走法, 白棋在 \(k\) 步之内取胜. 应该知道 \(k\) 须得为奇数. 这就是典型的规划问题. 我们以 QBF 的形式对象棋问题进行建模.
| \(\rm 标识符\) | \(\rm 意义\) |
|---|---|
| \(x_{\{m,n,i\}}\) | 棋子 \(m\) 第 \(i\) 步骤在棋盘上所处的位置 \(n\), 其中 \(1\le m\le 4s, 0\le n\le s^2, 0\le i\le k\). |
| \(I_0\) | \(x_{\{m,n,0\}}\) 变量上的子句集合, 表示棋盘的初始状态. |
| \(T^w_i\) | \(x_{\{m,n,i\}}, x_{\{m,n,i+\}}\) 变量上的子句集合, 表示白棋在步骤 \(i\) 的有效移动. |
| \(T^b_i\) | \(x_{\{m,n,i\}}, x_{\{m,n,i+\}}\) 变量上的子句集合, 表示黑棋在步骤 \(i\) 的有效移动. |
| \(G_k\) | \(x_{\{m,n,k\}}\) 变量上的子句集合, 表示棋局的目标, 比如说, 在 \(k\) 步之内, 黑棋的国王被白棋吃掉. |
由此可以公式化该问题, 得到公式: \[ \begin{align*} &\exists\{x_{\{m,n,0\}}\}\exists\{x_{\{m,n,1\}}\}\forall\{x_{\{m,n,2\}}\}\exists\{x_{\{m,n,3\}}\}...\forall\{x_{\{m,n,k-1\}}\}\exists\{x_{\{m,n,k\}}\}.\\ &I_0\land ((T^b_1\land T^b_3\land ...\land T^b_{k-2}) \Longrightarrow (T^w_0\land T^w_2\land ...\land T^w_{k-1}\land G_k)). \end{align*} \] 其实, 该公式并不能够很好的对问题进行描述. 由于僵局出现的可能性: 可能存在这样一种情况, 黑方无法采取有效措施, 导致平局. 在这种情况下上面的公式是有效的, 尽管它是不应该有效的. 该问题的可能解决方案是通过适当地修改 \(T^w\) 来禁止白棋进行导致这种状态的走法.
1.2 量化析取线性演算
量化析取线性演算(quantified disjunctive linear arithmetic, QDLA)的文法定义如下: \[ \begin{aligned} formula&:formula\land formula\ |\ \neg formula\ |\ (formula)\ \\ &\;|\;predicate\ |\ \forall identifier.formula\\ predicate&:\Sigma_ia_ix_i\lt c. \end{aligned} \] 其中 \(c, a_i\) 为常数, \(x_i\)为实型变量. 比如说, 如下公式就是QDLA: \[ \forall x.\exists y.\exists z.((y+1\le x\hspace{1pc} \lor\hspace{1pc} z+1\le y )\hspace{1pc} \land\hspace{1pc} 2x+1\lt z). \]
2. 量词消除(Quantifier Elimination)
2.1 前束范式(prenex normal form)
首先定义针对量化公式的范式.
前束范式. 如果一个公式符合如下形式则称之为前束范式: \[ Q[n]V[n]...Q[1]V[1].\langle quantifier\mbox{-}free formula\rangle, \] 其中, 对于所有的 \(i\in\{1,2,...,n\}, Q[i]\in\{\forall, \exists\}\), \(V[i]\) 是一个变量. 我们将公式左侧的量化字符串称为量化前缀, 而将量化前缀右侧的无量词公式称为量化后缀.
引理. 对于每一个量化公式 \(\mathcal{Q}\), 存在一个前束范式形式的公式 \(\mathcal{Q}'\), 当且仅当 \(\mathcal{Q}'\) 为真时 \(\mathcal{Q}\) 为真.
对于量化公式的判定, 要先将其转换成前束范式. 例如下面的转换算法 1. \[ \begin{align*} &\mathbf{Algorightm\;1\;:}\;\text{PRENEX}\\ \\ &\mathbf{Input:}\quad\;\;\; \text{A quantified formula}\\ &\mathbf{Output:}\quad\text{A formula in prenex normal form}\\ \\ &\;1.\;\text{Eliminate Boolean connectives other than } \vee,\wedge, \text{and } \neg.\\ &\;2.\;\text{Push negations to the right across all quantifiers, using De Morgan's rules}.\\ &\;3.\;\text{If there are name conflicts across scopes, solve by renaming: give each variable}\\ &\quad\;\;\text{in each scope a unique name}.\\ &\;4.\; \text{Move quantifiers out by using equivalences such as}\\ \\ &\hspace{25mm}\phi_1\land Qx.\phi_2(x)\Longleftrightarrow Qx.(\phi_1\land\phi_2(x))\\ &\hspace{25mm}\phi_1\lor Qx.\phi_2(x)\Longleftrightarrow Qx.(\phi_1\lor\phi_2(x))\\ &\hspace{25mm}Q_1y.\phi_1(y)\land Q_2x.\phi_2(x)\Longleftrightarrow Q_1y.Q_2x.(\phi_1(y)\land\phi_2(x))\\ &\hspace{25mm}Q_1y.\phi_1(y)\lor Q_2x.\phi_2(x)\Longleftrightarrow Q_1y.Q_2x.(\phi_1(y)\lor\phi_2(x))\\ \\ &\;\;\;\;\ \text{where } Q,Q_1,Q_2\in\{\exists,\forall\}\;\text{are quantifiers},\; x\notin var(\phi_1),\;\text{and } y\notin var(\phi_2). \end{align*} \]
用一个例子说明该算法的执行过程. 考虑如下量化公式: \[ \mathcal{Q}:=\neg \exists x.\neg(\exists y.((y\Longrightarrow x)\land (\neg x\lor y))\land \neg \forall y,((y\land x)\lor (\neg x\land \neg y))). \] 在算法的第1,2步, 消除蕴含符号, 并将非运算符移到里边: \[ \forall x.(\exists y.((\neg y\lor x)\land (\neg x\lor y))\land \exists y.((\neg y\lor \neg x)\land (x\lor y))). \] 算法第3步, 因为有两个量词作用在变量 \(y\) 上, 所以要对其进行重命名: \[ \forall x.(\exists y_1.((\neg y_1\lor x)\land (\neg x\lor y_1))\land \exists y_2.((\neg y_2\lor \neg x)\land (x\lor y_2))). \] 最后, 算法第4步, 将公式中的所有量词移到公式前面: \[ \forall x.\exists y_1.\exists y_2.(\neg y_1\lor x)\land (\neg x\lor y_1)\land (\neg y_2\lor \neg x)\land (x\lor y_2). \] 我们假定在量词消除算法中, 输入的公式为前束范式.
2.2 量词消除算法(quantifier elimination algorithm)
量词消除算法的作用是将一个量化公式转换成等价的无量词的公式. 并不是每一个理论都有对应的量词消除算法. 实际上, 量词消除算法的存在通常意味着逻辑的可判定性, 然而并非所有理论都是可判定的. 存在一个消除量词的程序是显而易见的. 全称量词的消除可以向存在量词进行转换. 为此, 我们定义了投影(projection)的一般概念, 每个理论都必须具体化.
投影. 变量 \(x\) 从具有 \(n\) 个量词的前束范式的量化公式的投影, \[ \mathcal{Q}_1=Q[n]V[n]...Q[2]V[2].\exists x.\phi, \] 是一个公式 \[ \mathcal{Q}_2=Q[n]V[n]...Q[2]V[2].\phi' \] 其中\(x\notin var(\phi')\), \(\phi, \phi'\) 都是无量词公式, 那么 \(\mathcal{Q}_1, \mathcal{Q}_2\) 逻辑上等价.
如下, 算法是用于消除前束范式中所有量词的 PROJECTION 算法.
\[ \begin{align*} &\mathbf{Algorithm\;2:}\; \text{QUANTIFIER-ELIMINATION}\\ \\ &\mathbf{Input:}\quad \text{A sentence } Q[n]V[n]...Q[1]V[1].\phi,\; \text{where }\phi\;\text{is quantifier-free}\\ &\mathbf{Output:}\; \text{A (quantifier-free) formula over constants }\phi',\;\text{which is valid}\\ &\quad\quad\quad\quad\;\;\text{if and only if }\phi\;\text{is valid}.\\ \\ &\;1.\; \phi':=\phi;\\ &\;2.\; \mathbf{for}\; i:=1,...,n\; \mathbf{do}\\ &\;3.\; \quad\quad\mathbf{if}\; Q[i]=\exists\; \mathbf{then}\\ &\;4.\; \quad\quad\quad\quad \phi':=\;\; \text{PROJECT}(\;\; \phi', V[i]);\\ &\;5.\; \quad\quad\mathbf{else}\\ &\;6.\; \quad\quad\quad\quad \phi':=\neg\text{PROJECT}(\neg \phi', V[i]);\\ &\;7.\; \text{Return}\;\phi'; \end{align*} \]
用两个例子说明量词消除算法的执行.
量化布尔公式的量词消除
我们可以运用二元解析的技术对量词进行消除. 下面举例说明, 考虑如下公式: \[ \begin{align*} &\forall u_1.\forall u_2.\exists e_1.\forall u_3.\exists e_3.\exists e_2.\\ &(u_1\lor \neg e_1)\land (\neg u_1\lor \neg e_2\lor e_3)\land(u_2\lor \neg u_3\lor \neg e_1)\land(e_1\lor e_2)\land(e_1\lor \neg e_3). \end{align*} \] 通过解析在 \(e_2\) 上的第二个和第四个子句得到: \[ \begin{align*} &\forall u_1.\forall u_2.\exists e_1.\forall u_3.\exists e_3.\\ &(u_1\lor \neg e_1)\land (\neg u_1\lor \neg e_1\lor e_3)\land(u_2\lor \neg u_3\lor \neg e_1)\land(e_1\lor \neg e_3). \end{align*} \] 通过解析在 \(e_3\) 上的第二个和第四个子句得到: \[ \forall u_1.\forall u_2.\exists e_1.\forall u_3. (u_1\lor \neg e_1)\land (\neg u_1\lor e_1)\land(u_2\lor \neg u_3\lor \neg e_1). \] 通过消除 \(u_3\) 得到: \[ \forall u_1.\forall u_2.\exists e_1. (u_1\lor \neg e_1)\land (\neg u_1\lor e_1)\land(u_2\lor\neg e_1). \] 通过解析在 \(e_1\) 上的第一个和第二个子句, 与第二个和第三个子句得到: \[ \forall u_1.\forall u_2. (u_1\lor \neg u_1)\land (\neg u_1\lor u_2). \] 第一个子句是重言式, 因此可以直接移除. 接下来可以移除 \(u_1\) 和 \(u_2\), 这将导致空的子句. 因此该公式为假.
量化析取线性演算的量词消除
考虑如下量化的线性公式, \[ \forall x.\exists y.\exists z.(y+1\le x\hspace{1pc}\land\hspace{1pc}z+1\le y\hspace{1pc}\land\hspace{1pc}2x+1\le z). \] 消除 \(z\), 得到: \[ \forall x.\exists y.(y+1\le x\hspace{1pc}\land\hspace{1pc}2x+1\le y-1). \] 消除 \(y\), 得到: \[ \forall x.(2x+2\le x-1). \] 将全称量词转变成存在量词得到: \[ \neg \exists x.\neg(2x+2\le x-1). \] 化简得到: \[ \neg \exists x.x\gt -3. \] 可见原公式为假.