Почему введение этого квантора существования приводит к незавершенности?

Я только начинаю играть с Z3 самостоятельно, и я подумал, что одним интересным экспериментом будет создание поля из 3 элементов.

Поэтому я объявил свое поле 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 конечно (и в этом случае даже очень небольшой)? Почему зацикливается? и каков правильный способ выразить аксиому вычитаемости, предпочтительно таким образом, чтобы не потерять воспринимаемость в ее предполагаемом интуитивном значении?


z3 smt theorem-proving
person usib    schedule 08.07.2019    source источник
comment
Квантификаторы трудны, чередующиеся квантификаторы сложнее. Хотя у вас конечный (и небольшой) домен, z3 не в состоянии распознать это и, скорее всего, застрянет в кишках e-matcher. Такого рода проблемы просто не подходят для SMT-решения: я бы рекомендовал использовать подходящее средство доказательства теорем (например, Isabelle, Coq, Agda, HOL, Lean и т. д.) для работы с такого рода аксиоматизациями.   -  person alias    schedule 09.07.2019

Ответы (1)


arrow_upward
0
arrow_downward

Хотя @alias в целом прав со своим предложением, вы, тем не менее, можете использовать Z3, если хотите ослабить свою аксиоматизацию. Например.:

...
; subtractivity
(declare-fun SUB (S S) S)
(assert (forall ((a S) (b S) (x S)) (iff (= (ADD a x) b) (= (SUB b x) a))))

(check-sat)
(get-model)
person Malte Schwerhoff    schedule 07.08.2019