我有一组符号变量:
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求解器支持它?
它能和其他理论混合吗，比如线性算法?
这仍然是未解释函数，因为如果存在满足你的公理的函数，那么它将属于未解释函数理论。类似地，如果这样的函数不存在，则在未解释的函数中不存在。所以你所描绘的是可满足的当且仅当未解释函数中的问题是可满足的，所以这两个理论是同构的，即相同的。
假设你试图根据你的公理证明某些定理是有效的，求解器如何表示可满足的结果并不重要，因为sat结果对应于无效的模型。要使用SMT求解器证明您的定理，您应该断言您的公理，断言定理的否定，然后寻找一个不令人满意的结果。关于满意度和效度之间关系的更详细解释，请参见这个问题。
要使用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)