Изабель: Кувалда находит доказательство, но оно не работает

Вы задаете ряд вопросов, но я буду рассматривать ваш заголовок и второй абзац как суть вашей основной жалобы, и в итоге я дам пространный ответ, который можно резюмировать следующим образом:

• Кувалда - это часть арсенала, состоящего из трех частей,
• вы становитесь более опытным, с бесконечными экспериментами, методом проб и ошибок - это эвристика,
• отказ от использования многих доказательств, которые возвращает Кувалда, является важной частью использования Кувалды, и
• Параметры minimize и preplay_timeout могут сэкономить вам время и нервы, автоматически воспроизводя доказательства, что дает вам информацию о времени, а иногда показывает, что найденное доказательство не удастся.

Начиная со второго абзаца, вы говорите:

Часто у меня возникает проблема с тем, что Кувалда находит доказательство. Но потом я пробую, но доказательство не заканчивается. Думаю, Кувалда - одна из самых важных частей Изабель, ...

Кувалда важна, но я считаю ее частью арсенала, состоящего из трех частей:

1. Подробные шаги доказательства с использованием естественной дедукции.
2. Автоматические методы доказательства, такие как auto, simp, rule и т. Д. Большая часть этого будет составлять ваши собственные simp правила перезаписи и научиться использовать теоремы с rule и множеством других автоматических методов доказательства.
3. Кувалда вызывает автоматические программы доказательства теорем (АТФ). Шаги 1 и 2 с опытом используются для настройки Sledgehammer. Опыт очень важен. Вы можете использовать auto, чтобы упростить вещи, чтобы Кувалда преуспела, но вы можете не использовать auto, потому что он расширит формулы до тех пор, пока Кувалда не имеет шансов на успех.

... но потом становится неприятно, если доказательство терпит неудачу.

Итак, здесь ваши ожидания и мои ожидания от Sledgehammer расходятся. В наши дни, если меня раздражает, меня раздражает то, что мне придется работать более 30 секунд, чтобы доказать теорему. Если я очень разочарован тем, что конкретное доказательство Кувалды терпит неудачу, то это потому, что я безуспешно пытался доказать теорему часами или днями.

Использование Кувалды не для поиска доказательств, а для поиска хороших доказательств

Иногда автоматизация может облегчить разочарование. Нажатие на доказательство кувалды только для того, чтобы узнать, что оно не работает, было бы неприятно. Вот как я сейчас использую Кувалду, если только я не начну отчаянно нуждаться в доказательствах:

sledgehammer_params[minimize=smart,preplay_timeout=10,timeout=60,verbose=true,
                    max_relevant=smart,provers="
  remote_vampire  metis  remote_satallax  z3_tptp  remote_e
  remote_e_tofof  spass  remote_e_sine    e        z3       yices
"]

Опции minimize=smart и preplay_timeout=10 относятся к тому, что Кувалда воспроизводит доказательства после того, как найдет их. Отказ от использования многих доказательств, которые находит Кувалда, является важной частью использования Кувалды, а воспроизведение доказательств - большая часть отбраковки доказательств.

Лично я не особо разбираюсь в доказательствах Sledgehammer, которые не обрываются, но это, вероятно, потому, что я с самого начала избирательный.

Мой первый критерий для доказательства Sledgehammer - это то, что оно должно быть достаточно быстрым, и поэтому, когда Sledgehammer сообщает, что нашел доказательство продолжительностью более 3 секунд, я даже не пытаюсь его использовать, если только я не отчаянно пытаюсь выяснить, есть ли Теорема может быть доказана.

Обычно я использую Кувалду так:

• Сформулируйте теорему и посмотрите, повезет ли мне с Кувалдой.
• Если Sledgehammer предоставит мне доказательство продолжительностью 30 миллисекунд или меньше, то я считаю это хорошим доказательством, но я все еще экспериментирую с try и автоматизированными методами доказательства из раздела 9.4.4, стр. 208, isar-ref.pdf. Много раз я могу получить доказательство до 5 мс или меньше.
• metis доказательство общего времени более 100 мс, я готов работать 30 минут или больше, чтобы попытаться получить более быстрое доказательство.
• metis доказательство от 200 мс до 500 мс, я прибегну ко всему, что знаю, чтобы попытаться уменьшить его до менее 100 мс, что во многих случаях означает преобразование в подробное доказательство.
• smt или metis доказательство продолжительностью более 1 секунды я считаю хорошим только временным доказательством.
• Доказательство на панели вывода, которое, как сообщает Кувалда, превышает 3 секунды, я обычно даже не пытаюсь, потому что, даже если он закончится работать, мне все равно придется поработать, чтобы найти другое доказательство, поэтому я бы Лучше потратить свое время на поиски хорошего доказательства.

Вариант 3 эвристический

Ты говоришь,

Так что насчет третьего варианта. Есть ли какие-нибудь простые эвристики, которые я могу применить?

Эвристика:

• "по мере необходимости",

это означает, что эвристика состоит в том, чтобы «использовать кувалду как часть трехступенчатого арсенала».

Эвристика также заключается в том, чтобы «прочитать множество руководств и документации, чтобы у вас было много других вещей, которые можно использовать с Sledgehammer». Кувалда мощная, но не бесконечно мощная, и для некоторых теорем вы можете использовать свои собственные simp правила, чтобы доказать за 0 мс с apply(simp) или apply(auto) то, что Кувалда никогда не докажет.

Что касается меня, то я использую от 150 до 200 теорем, так что «по мере необходимости» имеет для меня гораздо большее значение, чем раньше. По сути, вы пытаетесь настроить Sledgehammer так, как нужно.

Способ настройки Sledgehammer иногда означает запуск auto или simp, но иногда нет, потому что много раз запуск auto или simp обрекает Sledgehammer на провал.

Но иногда вам даже не нужно metis доказательство от Sledgehammer, кроме как в качестве предварительного доказательства, пока вы не найдете лучшее доказательство, что для меня обычно означает более быстрое доказательство с использованием методов автоматического доказательства.

Я не специалист по Кувалде, но кажется, что Кувалда хорош в сопоставлении гипотез и выводов из старых теорем с гипотезами и выводами, используемыми для новой теоремы. В чем он не хорош, так это в доказательстве формул, которые я значительно расширил, используя simp и auto.

Я продолжаю длинную эвристику, ориентированную на Кувалду:

• Используйте Sledgehammer, чтобы ускорить процесс доказательства, доказывая с помощью Sledgehammer некоторые теоремы, которые вы иначе не знаете, как доказать.
• Превратите ваши эквивалентные теоремы в simp правила перезаписи для использования с такими автоматическими методами доказательства, как simp, auto, fastforce и т. Д., Как описано в главе 9 файла tutorial.pdf.
• Используйте некоторые из ваших теорем для правил условной перезаписи для использования с intro и rule.
• Последние два шага используются для полного решения шага проверки или используются для настройки Sledgehammer «по мере необходимости». Кувалда никогда не перестает быть полезной, независимо от того, сколько вы знаете, и она чрезвычайно полезна, когда вы мало знаете, но одна только Кувалда не путь к успеху.
• Если Кувалда не может доказать теорему, прибегните к подробному доказательству, начиная с простого подробного доказательства. Иногда разделение «если и только если» на два условия позволяет Кувалде легко доказать эти два условия, хотя он не может доказать «если и только если».
• После того, как вы доказали много вещей, вернитесь и оптимизируйте свои доказательства. Иногда со всеми созданными вами правилами перезаписи simp и auto волшебным образом доказывают вещи, и вы избавляетесь от некоторых metis доказательств, которые Кувалда нашла для вас. Иногда вы будете использовать Кувалду, чтобы найти metis доказательство, которое еще быстрее.

Используйте эту команду для оптимизации времени:

ML_command "Toplevel.timing := true"

Есть еще один пост SO, в котором более подробно рассказывается об этом.

Могу ответить на ваш подвопрос «В чем разница между unfolding и using?». Грубо говоря, это работает так.

Предположим, что лемма foo имеет вид x = a+b+c. Если вы напишете

unfolding foo

в вашем доказательстве все вхождения x будут заменены на a+b+c. С другой стороны, если вы напишете

using foo

тогда x=a+b+c будет добавлен к вашему списку предположений.