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

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)