命题逻辑

Question

我有以下问题：

我有两个命题公式，它们在逻辑上是等价的。只有其中一个包含一个“变量”，即该变量可以被任何命题公式替换。现在的问题是，我需要找到这个变量的实际替换，这样逻辑等价就变成了真。示例：

(a ^ ~b)或x=a

这里，x表示变量。通过将x替换为a^ b，可以实现这种逻辑等价，因此它变成了：

(a ^ ~b)或(a ^ b) =a

所以这就是问题所在。我需要一个算法作为输入，得到“一个变量x的方程”，并给出变量x的输出值，这样方程就变成了逻辑等价。

总有一个变量。(事实上，我可能会遇到多个变量的问题，但我想先解决简单的情况)。这些公式可以有任何形式(它们不在CNF或DNF中)。此外，公式实际上可以是假的或真的，而且在某些情况下，没有解(例如，对于"a或x= false"，没有解)或多个解(例如，对于"a和x= false“，任何虚假命题都是有效的答案)。

我所拥有的只是一个表格推理者，它告诉我一个公式是否可以满足。这样我就可以测试一个解决方案了。但我的问题是给我一个解决办法。

Answer 1

我相信你要找的是一个能处理未解释函数的推理引擎。这样的引擎可以处理包含函数的问题，例如，

(a ^ ~b)或f(a，b) =a

它们通常能够生成模型，也就是说，它们实际上会生成一个函数f(.)满足你最初的公式。合适的推理引擎的一个例子就是所谓的SMT求解器(参见SMT-LIB)。一个流行的解决方案是微软的Z3 (参见Z3)。

这个例子可以用SMT-LIB格式表述如下：

(set-option :produce-models true)
(declare-const a Bool)
(declare-const b Bool)
(declare-fun f (Bool Bool) Bool)

(assert (= (or (xor a (not b)) (f a b)) a))
(check-sat)
(get-model)
(exit)

Z3生成模型

(define-fun f ((x!1 Bool) (x!2 Bool)) Bool 
  (ite (and (= x!1 false) (= x!2 true)) false false))

满足了原来的问题。通常情况下，解决方案只满足这个问题。为了得到完整的解决方案，可以使用量词。并不是所有的SMT求解器都支持它们，但是Z3使用了一个完整的在有限域上的量词推理引擎(比如Booleans)，并且能够为这样的公式生成模型。