Я только начинаю играть с Z3 самостоятельно, и я подумал, что одним интересным экспериментом будет создание поля из трех элементов.
Поэтому я объявил, что мое поле S является скалярным перечислением трех элементов, A, B, C, и начал постепенно добавлять аксиомы поля, запрашивая модель Z3 после каждого шага, просто чтобы посмотреть, что происходит.Все идет хорошо, пока я не утверждаю возможность вычитания, ∀ab. (∃x.a + x = b):
(declare-datatypes () ((S A B C)))
; there exist three distinct elements in S
(declare-const someA S)
(declare-const someB S)
(declare-const someC S)
(assert (distinct someA someB someC))
(declare-fun ADD (S S) S)
(declare-fun MUL (S S) S)
; commutative
(assert (forall ((x S) (y S)) (= (ADD x y) (ADD y x))))
(assert (forall ((x S) (y S)) (= (MUL x y) (MUL y x))))
; associative
(assert (forall ((x S) (y S) (z S)) (= (ADD x (ADD y z)) (ADD (ADD x y) z))))
(assert (forall ((x S) (y S) (z S)) (= (MUL x (MUL y z)) (MUL (MUL x y) z))))
; subtractivity
(assert (forall ((a S) (b S)) (exists ((x S)) (= (ADD a x) b))))
(check-sat)
(get-model)
Это приводит к циклу Z3 навсегда.Я удивлен.Я имею в виду, да, я понимаю, почему FOL в общем неразрешима, но я думаю, что это будет один из тех «простых» случаев, потому что пространство всех возможных значений для a, b и ADD конечно (и в этом случае даже оченьмаленький)?Почему это петля?и как правильно выразить аксиому вычитаемости предпочтительно так, чтобы она не теряла воспринимаемости в качестве ее предполагаемого интуитивного значения?