Prover9 «Некоторые, но не все, запрошенные доказательства были найдены» - PullRequest
Новая
       22

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

0 голосов
/ 27 июня 2019

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

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

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

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

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

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

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

1 Ответ

1 голос
/ 01 июля 2019

Я воспроизвел это после долгих попыток, но только установив какой-то странный параметр, который, я уверен, я бы не трогал.(Единственный вариант, который я обычно меняю, - это 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подэкран, когда я в конце концов нашел его.Weird.

...