разрешима ли теория списка?

Мне интересно, разрешима ли теория списка z3? Кажется, что мы можем доказать только факты, которые не подтверждены, но не подтверждены с помощью теории, поэтому мне любопытно, разрешима ли она на самом деле. Спасибо за вашу помощь.


z3
person JRR    schedule 07.06.2012    source источник
comment
Не могли бы вы привести примеры фактов, которые вы не можете доказать? Вы используете квантификаторы?   -  person Leonardo de Moura    schedule 07.06.2012
comment
Да, например, в примере (stackoverflow.com/questions/10642565/cross-product-in-z3) вы дали ранее, пытаясь доказать (assert (= (first (head l)) a)) в значительной степени не завершится. Поэтому мне интересно, имеет ли это отношение к теории списков или кванторов в целом.   -  person JRR    schedule 07.06.2012

Ответы (1)


arrow_upward
1
arrow_downward

В Z3, когда мы говорим, что теория разрешима, мы обычно говорим о бескванторных задачах. Теория списка, реализованная в Z3, разрешима. Однако, как только мы используем квантификаторы и неинтерпретируемые функции, как в вопросе перекрестное произведение в z3, проблема становится неразрешимой. Z3 может решать некоторые фрагменты, но проблема, описанная в перекрестном произведении в z3, отсутствует ни в одном фрагменте. поддерживается Z3. На самом деле, Z3 не сможет построить модель для какой-либо задачи, подобной этой. Таким образом, он будет вечно работать, пытаясь построить модель, или перестанет возвращать unknown. Результат unknown все еще может быть полезен. В некоторых случаях Z3 может создать «модель-кандидат». То есть интерпретация, которая не удовлетворяет всем универсальным формулам в вашей задаче, но удовлетворяет всем бескванторным формулам и многим экземплярам универсальных формул. Для этого нам нужно отключить модуль MBQI. Когда MBQI включен, Z3 будет пытаться найти интерпретацию, которая удовлетворяет всем квантификаторам. Вот как мы это делаем для вас, например:

http://rise4fun.com/Z3/kGtk

Хитрость заключается в следующих двух командах, которые я включил в начало скрипта:

(set-option :auto-config false)
(set-option :mbqi false)

Я использовал команду get-value, чтобы показать, что интерпретация, созданная Z3, удовлетворяет (assert (= (first (head l)) a)). С другой стороны, интерпретация для append на самом деле не удовлетворяет универсальным формулам в этом примере.

person Leonardo de Moura    schedule 07.06.2012