我有一组符号变量：
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 求解器支持它？
它可以与其他理论混合，比如线性算术吗？
This is still uninterpreted functions, because if there exist functions that satisfy your axioms then this would be sat in the theory of uninterpreted functions. Similarly, if such functions do not exist, then this is unsat in uninterpreted functions. So what you are picturing is satisfiable if and only if the problem in uninterpreted functions is satisfiable, so the two theories are isomorphic, i.e. the same.
Given that you're trying to prove that certain theorems are valid based on your axioms, it shouldn't matter how the solver represents a satisfiable result, because sat results correspond to invalid models. To prove your theorems using an SMT solver, you should assert your axioms, assert the negation of the theorem, and then look for an unsatisfiable result. See this question for a more detailed explanation of the connection between satisfiability and validity.
To prove your first theorem using Z3, the following suffices in 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)