Есть ли теория неинтерпретируемых функций (конгруэнтный анализ)?

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

Это все еще неинтерпретированные функции, потому что, если существуют функции, которые удовлетворяют вашим аксиомам, то это будет отражено в теории неинтерпретированных функций. Точно так же, если такие функции не существуют, то это не подходит для неинтерпретируемых функций. Итак, то, что вы изображаете, выполнимо тогда и только тогда, когда проблема в неинтерпретируемых функциях выполнима, поэтому две теории изоморфны, то есть одинаковы.

Учитывая, что вы пытаетесь доказать, что определенные теоремы действительны на основе ваших аксиом, не должно иметь значения, как решатель представляет удовлетворительный результат, потому что сат результаты соответствуют недействительным моделям. Чтобы доказать свои теоремы с помощью 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)