Во-первых, я бы рекомендовал подписаться на список рассылки пользователя Isabelle, чтобы следить за информацией об этих вещах. В частности, в течение последних шести месяцев, были темы о Sledgehammer
- как
sledgehammer связано с try,
- как
Auto methods в Isabelle/Options связано с try,
- как многопоточность влияет
try и sledgehammer,
- , как устанавливаются опции и указатели для панели Кувалда, которые можно использовать для запуска кувалды,
- как количество ядер ЦП влияет на то, как параметры автоматически устанавливаются для
sledgehammer,
- и вообще как для каждого из них выбраны кувшины различными способами, некоторые автоматические.
Это все связано с вашим вопросом, где один короткий ответ на вопросы, что две большие вещи, которые влияют на sledgehammer выход есть варианты и многопоточность, где вы можете только полностью контролировать sledgehammer варианты, давая ему возможности когда вы его используете, или путем установки параметров с помощью sledgehammer-params.
Ниже я приведу несколько ссылок на список рассылки, где вчерашний день М. Ванзель дал краткое объяснение автоматическим настройкам Кувалды.
Еще один ответ на ваш второй вопрос: команда try представляет собой многопоточную комбинацию из try0 и sledgehammer. Есть параметры по умолчанию sledgehammer, которые можно просмотреть с помощью sledgehammer_param. Если вы не изменили эти параметры, тогда команда sledgehammer, используемая в вашей теории, будет использовать эти параметры. Является ли try этими опциями, я не знаю, но я покажу вам, как определить, дает ли trysledgehammer провер, который не указан в параметрах по умолчанию.
Я предполагаю, что try работает для вас, как будто это работает для меня.
Сначала вставьте sledgehammer_params и посмотрите на выходную панель. Он покажет вам provers. Мое значение по умолчанию: e spass vampire z3, потому что у меня 4 ядра. Они были выбраны при запуске PIDE. Это те же самые указатели, которые будут показаны на панели Sledgehammer. Вторым важным вариантом будет timeout = 30.
Когда я вставляю try для теоремы, try0 методы не могут доказать, и который sledgehammer может, наряду с каждым by доказательством того, что перечислено в панели вывода, он сообщит мне ATP (автоматическая теорема Доказывающий), которая найдена доказательство. Например, моя показывает мне "e", "z3" и "spass", за каждым последует доказательство.
Ответ: Если try показывает АТФ, что нет в списке, когда вы используете sledgehammer_params, то try дает sledgehammer другой provers вариант, чем при запуске sledgehammer с параметрами по умолчанию.
Запуск прувер, которые пытаются перечисленным: Для того, чтобы ответить на ваш вопрос о том, можно ли получить sledgehammer дать вам то же sledgehammer доказательства того, что try дает вам, запускать отдельные прувер, что перечисленные try, например, как это:
sledgehammer[provers = "z3", timeout = 60]
Я показываю timeout просто чтобы показать, что вы можете изменить его, но как правило, не требуется больше тайм-аут, потому что try не пытается вещи навсегда.
Если явное использование sledgehammer дает вам z3 доказательства, когда try дал вам z3 доказательства, то это говорит о том, что это варианты и многопоточность, которые влияют на различные результаты. Я определенно знаю, что выход sledgehammer и nitpick сильно различается.
Я не использую try. Я использую try0 и sledgehammer, но то, что вы говорите, показывает, что автоматически заданные параметры для автоматических методов лучше. Авто nitpick находит контрпримеры, которые nitpick не находит, потому что я изменил параметры для nitpick.
Ссылки