是否存在不可解釋函數的理論（同餘分析）？

Question

我有一組符號變量的：

int a, b, c, d, e; 

一組未知函數，由若干公理的約束：

f1(a, b) = f2(c, b) 
f1(d, e) = f1(e, d) 
f3(b, c, e) = f1(b, e) 
c = f1(a, b) 
b = d 

在此功能f1，f2，f3是未知的，但固定的。所以它不是uninterpreted functions的理論。

我要證明以下斷言的有效性：使用基於上面的等式公理換人

c = f2(f1(a, b), b) 
f3(d, f2(c, b), e) = f1(e, b) 

。

有沒有理論，對於這樣的定理，只會使用提供的平等來試圖結合答案，而不是提出解釋的功能？

如果是這樣，理論的名稱是什麼，SMT解算器支持什麼？

它可以與其他理論，如線性算術混合嗎？

Answer 1

這仍然是未解釋的函數，因爲如果存在滿足您的公理的函數，那麼這將是未解釋函數的理論。同樣，如果這些功能不存在，那麼這在未解釋的功能中是不可接受的。所以你所描繪的是可滿足的，當且僅當未解釋函數中的問題是可滿足的，所以這兩種理論是同構的，即相同的。

鑑於您試圖基於您的公理證明某些定理是有效的，所以求解器如何代表可滿足結果並不重要，因爲sat結果對應於無效模型。爲了用SMT解算器證明你的定理，你應該斷言你的公理，斷言定理的否定，然後尋找一個不可取的結果。有關可滿足性和有效性之間的聯繫的更詳細解釋，請參見this question。

要使用Z3證明你的第一個定理，在SMT-LIB 2以下就足夠了：

(declare-fun a() Int) 
(declare-fun b() Int) 
(declare-fun c() Int) 

(declare-fun f1 (Int Int) Int) 
(declare-fun f2 (Int Int) Int) 

(assert (= (f1 a b) (f2 c b))) 
(assert (= c (f1 a b))) 
(assert (not (= c (f2 (f1 a b) b)))) 

(check-sat)