действительно ли «двойная стрелка» =› означает «подразумевается»?

Делает

(=> (f g))

всегда означает то же самое, что и

(or (not f) g))

?

Два выражения ведут себя по-разному в моей модели. В то время как использование => дает мне UNSAT, использование другого варианта не дает никакого результата (время ожидания). Я был бы доволен, если бы у меня был список операторов и их значений. Я знаю о стандарте SMTLIB, но в документах явно не говорится о значениях операторов. В частности, «=>», по-видимому, удваивается как псевдоним для оператора «ite» (if_then_else), если он используется в троичном выражении, и я совершенно смущен этим.

Я устанавливаю логику AUFLIA, если это уместно.

Сначала я ищу простой ответ да или нет. И во-вторых, правильная документация по SMT2 (возможно, книга).

У меня есть эта довольно большая модель, сгенерированная на основе модели Marksweep Дэниела Джексона для сплава4 для тех из вас, кто желает видеть для себя.


z3 smt
person Jonny    schedule 25.07.2012    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Ваши выражения неверны/неправильны.

=> действительно означает «подразумевается». Другими словами, (=> f g) эквивалентно (or (not f) g).

Если вы сомневаетесь, вы можете доказать это с помощью Z3. Следующий запрос — unsat:

(declare-const p Bool)
(declare-const q Bool)

(define-fun conjecture () Bool
    (= (=> p q) 
       (or (not p) q)))

(assert (not conjecture))
(check-sat)
person pad    schedule 25.07.2012
comment
Спасибо. Он действительно был деформирован. - person Jonny; 25.07.2012