Is there a theory for uninterpretable functions (congruence analysis)?

Question

I have a set of symbolic variables:

int a, b, c, d, e;

A set of unknown functions, constrained by a number of axioms:

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

Here functions f1, f2, f3 are unknown, but fixed. So it is not a theory of uninterpreted functions.

I want to prove validity of the following assertions:

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

using substitutions based on the axiomatic equalities above.

Is there a theory, for such theorems that would only use the provided equalities to try to combine the answer, rather than coming up with interpretation for the functions?

If so, what is the name of the theory, and what SMT solver does support it?

Can it be mixed with other theories, like linear arithmetic?

Answer 1

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)