命題邏輯

Question

我有以下問題：

我有兩個命題公式必須在邏輯上等價。只有其中一個包含一個'變量'，因爲變量可以被任何命題公式所取代。現在的問題是，我需要找到變量的實際替代，以使邏輯等價變爲真。例如：

（一個^〜b）或X = A

在此，x表示該變量。這個邏輯等價可由真實的，通過用^ B更換的x，所以它成爲：

（一個^〜B）或（a^B）=一個

因此，這就是問題所在。我需要一種算法，得到作爲輸入的「與一個變量x方程」，並給出作爲變量x，使得方程變爲邏輯等價輸出值。

總是會有一個變量。 （事實上​​，我可能會遇到多個變量的問題，但我想先解決這個簡單的問題）。所涉及的公式可以有任何形式（它們不在CNF或DNF中）。此外，公式實際上可以是FALSE或TRUE，並且存在這樣的情況時，有沒有溶液（例如，對於「一個或x =假」，沒有溶液）或多於一個的解決方案（例如用於「a和x =假「任何錯誤的主張都是有效的答案）。

我只有一個舞臺造型推理，告訴我一個公式是否可滿足與否。這樣我就可以測試的解決方案。但我的問題是給我一個解決方案。

Answer 1

我相信你正在尋找的是一個推理引擎可以處理未解釋功能。這樣的發動機可以處理包含函數的問題，例如，

（一個^〜B）或f（A，B）=一個

並且它們通常是能夠生產的機型，即，它們實際上將產生函數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例如使用完整的推理引擎來處理有限域上的量詞（如布爾），並且能夠爲這些公式生成模型。