Prover9 Некоторые, но не все запрошенные доказательства были найдены

Я запускаю некоторые доказательства решетки через Prover9/Mace4. Prover9 говорит Exit: Time limit. плюс сообщение в Заголовке.

Я удвоил лимит времени с 60 до 120 секунд. То же сообщение (в два раза быстрее). Странно вот что:

  • есть только одно утверждение, которое нужно доказать. То есть в отчете только одна label(goal) (что с but not all?)
  • похоже, что доказательство завершено, поскольку показывает последнюю строку $F.
  • Mace4 не может найти контрпримеров (я увеличил время до 120 секунд).

Я нашел несколько GHits для этого сообщения, но, кажется, все они на китайском (?)

Возможно, приведенные мною аксиомы (взаимно) рекурсивны — я пытаюсь ввести функцию и назначенный «поглощающий элемент» [**]; и это решение потребует бесконечного объединения. Prover9 делает это?

Я рад добавить аксиомы и цель к этому сообщению. (Я использую нестандартный способ определения встречи и присоединения.) Но во-первых, нужно ли мне пройти какие-либо проверки работоспособности?

[**] поглощающий элемент не является ни верхом, ни низом решетки; больше похоже на решетку левый угол. (Элемент будет низом решетки только в том случае, если решетка вырождается до двух элементов.) Функция представляет собой частичное упорядочение «под прямым углом» к верху/низу. Я ожидаю, что решетка не будет ни дополняемой, ни дистрибутивной (опять же, за исключением случаев, когда 2 элемента).


logic theorem-proving
person AntC    schedule 27.06.2019    source источник
comment
Prover9 доказывает от противного, поэтому $F указывает на то, что противоречие найдено, таким образом указывая на то, что доказательство существует. Можете ли вы точно опубликовать то, что вы дали Prover9, включая цели и предположения?   -  person Doug Spoonwood    schedule 01.07.2019
comment
Смотрите ответ, который я опубликовал, спасибо @Doug и приносим извинения за ложную тревогу. Я думаю, что это не имело ничего общего с конкретными предположениями/целями.   -  person AntC    schedule 01.07.2019
comment
Кстати, есть ли смысл использовать Prover9? После смерти Билла МакКьюна в 2009 году он больше не развивался. Есть E Prover и Vampire, например.   -  person lambda.xy.x    schedule 01.07.2019
comment
Есть ли причина не использовать Prover9? Это работает (для моих целей). Логика вечна. Зачем мне что-то развиваться дальше?   -  person AntC    schedule 01.07.2019
comment
Причины против использования EProver или Vampire: см. их страницы загрузки; недоступно для Windows; на самом деле они, кажется, не знают о Windows как о платформе. Я не хочу заниматься компиляцией программного обеспечения в среде UNIX; Я хочу запустить пруфы. Я посмотрю еще раз, когда они будут готовы к прайм-тайму.   -  person AntC    schedule 01.07.2019
comment
Доказательство 9 — прекрасный решатель, он может просто истечь время на больших проблемах (в частности, с равенством, из-за того, что Доказательство 9 не основано на исчислении суперпозиции). Если вы хотите проверить свою проблему с помощью набора решателей в Интернете, вы также можете использовать System on TPTP.   -  person lambda.xy.x    schedule 01.07.2019
comment
Кстати, насчет прайм-тайма: E и Vampire — передовые пруверы в своей области, вот почему я упомянул их.   -  person lambda.xy.x    schedule 01.07.2019
comment
Доказательство 9 не основано на исчислении суперпозиций, хм? В руководстве/глоссарии Prover9 упоминается суперпозиция, а здесь cs.unm.edu/~mccune/prover9/manual/2009-11A/inf-rules.html цитирует Bachmair-Ganziger-res и Nieuwenhuis-Rubio-res, оба из Справочника 2001 года.   -  person AntC    schedule 02.07.2019
comment
Доказательство 9 выполняет парамодуляцию, пишет справочник. В отличие от суперпозиции правил вывода, это правило вывода касается светлых сторон уравнений. Оно делает упорядоченное разрешение, но именно поэтому я указал на рассуждения о равенстве.   -  person lambda.xy.x    schedule 03.07.2019

Ответы (1)


arrow_upward
1
arrow_downward

Я воспроизвел это после долгих попыток, но только установив какую-то странную опцию, которую, я уверен, я бы не трогал. (Единственный вариант, который я обычно меняю, это Time limit, а я Reset to defaults довольно часто, так что это смахнуло бы все доказательства.)

Вот мое предположение о том, что произошло.

что с but not all?

  • Вы можете ввести несколько целей (при условии, что все они положительные). [**]

  • При странных настройках опций, если Prover9 может доказать первое, но не второе, он будет продолжать попытки, пока не будет исчерпан; но затем сообщайте только об успешном - с результатом $F. OK.

  • Если вы удвоите ограничение по времени, оно все равно докажет первое и продолжит попытки для второго — потребуется вдвое больше времени для того же результата.

  • Mace4 наткнется на первую цель и потратит время на поиск контрпримера. Его нет, потому что это доказуемо. Опять же, удвоение его лимита времени даст тот же результат после удвоения времени.

[Примечание **] Я никогда не намереваюсь ставить несколько целей; но когда я взламываю/экспериментирую с аксиомами, я держу все цели в поле Goals:, чтобы легко переключать un/comment. Думаю, я не прокомментировал один, когда раскомментировал другой.

Как правило, как описано в руководстве, Prover9 сообщает об успешном достижении первой цели, которую он доказывает; не идет к другим целям. Если есть несколько доказуемых целей, кажется, что выбирается самая простая/быстрая(?) независимо от позиции в файле.

Но если для max_proofs установлено значение больше, чем по умолчанию 1 , Prover9 продолжит попытки. (Есть также флаг auto_denials, который как-то связан с этим, я не понимаю.)

Я понятия не имею, как я установил max_proofs — я не узнал подэкран Options/Limits, когда в конце концов нашел его. Странный.

person AntC    schedule 01.07.2019
comment
В общем, старайтесь иметь только одну гипотезу - специалисты по доказыванию теорем расходятся во мнениях относительно того, как с ними обращаться (конъюнкция или дизъюнкция), так что стандарт TPTP в конечном итоге определяет семантику только для одной гипотезы. - person lambda.xy.x; 01.07.2019
comment
Более того, в TPTP есть концепция включаемых файлов, которые можно использовать совместно с общим набором аксиом, если вы хотите доказать несколько предположений. - person lambda.xy.x; 01.07.2019
comment
Да, я стремлюсь к одной цели. По этому поводу я запутался. - person AntC; 01.07.2019