Подсказки Prover9 не используются

Я запускаю некоторые доказательства решетки через Prover9/Mace4. Я использую нестандартную аксиоматизацию операции решеточного соединения, из которой сразу не следует, что соединение является коммутативным, ассоциативным и идемпотентным. (Я могу заставить Prover9 доказать, что это так — в конце концов.)

Я знаю, что Prover9 ищет эти свойства, чтобы ускорить поиск. Я попытался поместить эти свойства в раздел «Дополнительный ввод» (я использую графический интерфейс версии 0.5) с помощью

formulas(hints).
x v y = y v x.
% etc
end_of_list.

Q1: Это способ заставить его смотреть на подсказки?

Q2: Есть ли хорошее место, где можно найти помощь по ускорению доказательств/советы и приемы? (Если я смогу заставить это работать, есть и другие операторы, для которых я хотел бы дать подсказки.)

Для справки, мои аксиомы (двойная решетка только с одной примитивной операцией):

x ^ y = y ^ x.                % lattice meet
x ^ x = x.
(x ^ y) ^ z = x ^ (y ^ z).
x ^ (x v y) = x.              % standard absorption for join
x ^ z = x & y ^ z = y <-> z ^ (x v y) = (x v y).
                              % non-standard absorption

(EDIT после публикации ответа DougS.)

Ух ты! Спасибо. Ускорение на порядки величины.

Некоторые последующие вопросы, если можно...

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

Q4: Что, если я добавлю подсказки, которые (как оказалось) не подтверждаются аксиомами? Их игнорируют?

Q5: Что, если я добавлю подсказки, противоречащие аксиомам? (Исходя из нескольких испытаний, это не делает Prover9 неправильным выводом.)

Q6: Для доказательства (попытки), время ожидания которого истекло, есть ли способ получить формулы, выведенные до сих пор, и переработать их для подсказок, чтобы ускорить следующую попытку? (У меня есть ощущение, что это приведет к какой-то ошибке, несмотря на то, что я видел в отношении Q3 и Q4.)


logic theorem-proving
person AntC    schedule 11.06.2014    source источник
comment
(Спасибо за улучшение моих тегов.) Мне интересно, можно ли задать этот вопрос в stackoverflow? Возможно, math.stackexchange?   -  person AntC    schedule 11.06.2014
comment
Моя электронная почта: [email protected] ... вы также можете написать мне, если хотите.   -  person Doug Spoonwood    schedule 13.06.2014

Ответы (2)


arrow_upward
2
arrow_downward

Q3: Да, вы должны ожидать, что аксиома(ы) и цель(и) включены в качестве подсказок. Оба они могут служить полезными. Я больше имел в виду, что вы можете увидеть что-то вроде «$F», поскольку подсказка, похоже, мало что мне добавляет, и эти подсказки также сначала ведут вас по определенному пути, который может затруднить или упростить поиск более коротких доказательств. Однако, если вам просто нужно более быстрое доказательство, то, вероятно, лучше всего использовать все предложенные подсказки.

Q4: Подсказки НЕ должны быть выведены из аксиом.

Q5: Подсказки могут противоречить аксиомам, конечно.

В руководстве говорится: «Производное предложение соответствует подсказке, если оно включает в себя подсказку.

...

Короче говоря, значение по умолчанию для параметра hints_part указывает на выбор предложений, которые соответствуют подсказкам (сначала самые легкие), когда они доступны».

«Пункт C включает в себя пункт D, если переменные C могут быть реализованы таким образом, что он становится подпунктом D. Если C включает D, то D можно отбросить, потому что он слабее или эквивалентен C. (Есть некоторые процедуры проверки, которые требуют сохранения включенных пунктов.)"

Допустим, вы положили

 1. x ^((y^z) V v)=x V y as a hint.

Тогда, если Prover9 генерирует

 2. x ^ ((x^x) V v)=x V x

x ^ ((x^x) V v)=x V x будет выбран всякий раз, когда он доступен, поскольку он соответствует подсказке.

Это объяснение не является полным, потому что я не совсем уверен, как определяется «подпункт».

Тем не менее, вместо создания формул с исходными аксиомами и любой процедурой, используемой Prover9 для создания формул, формулы, соответствующие подсказкам, будут помещены в начало списка для создания формул. Это может ускорить работу программы, но из того, что я читал о некоторых других проблемах, кажется, что многие сложные проблемы в основном не были бы решены автоматически, если бы не такие вещи, как подсказки, взвешивание и другие стратегии. .

Q6: Я не уверен, какие формулы вы имеете в виду. В Prover9, конечно, вы можете нажать «показать вывод» и просмотреть десятки сгенерированных формул. Вы также можете установить леммы, которые считаете полезными, в качестве дополнительных целей, а затем использовать Prooftrans для создания подсказок из этих лемм, чтобы использовать их в качестве подсказок при следующем запуске. Или вы можете использовать этапы доказательства этих лемм как подсказки для следующего запуска. Если вы используете этапы этих доказательств в качестве подсказок или подсказки, предложенные Prooftrans, нет ошибки в рассуждениях, потому что подсказки на самом деле не добавляют никаких предположений к исходному набору. Механизм подсказки работает, по крайней мере, согласно моему приблизительному пониманию, путем изменения процедуры поиска, чтобы использовать предложение, которое соответствует подсказке, как только у нас есть что-то, что соответствует подсказке (то есть программа должна вывести что-то, что соответствует подсказке, и только тогда можно использовать то, что соответствует подсказке).

person Doug Spoonwood    schedule 16.06.2014

arrow_upward
2
arrow_downward

Q1: Да, это должно работать для подсказок. Но, чтобы лучше проверить это, возьмите доказательство, которое у вас есть, а затем используйте опцию «переформатировать» и проверьте часть «подсказок». Затем скопируйте и вставьте все эти подсказки в свои «формулы (подсказки)». список. (ну, вам не обязательно нужны все они... и использование только некоторых из них может привести к более короткому доказательству, если оно существует, но я отвлекся). Затем запустите доказательство еще раз, и если оно пройдет так же, как мои доказательства в исчислении высказываний с подсказками, вы получите доказательство «в одно мгновение».

На всякий случай... вам нужно нажать на вкладку "дополнительный ввод" и поместить туда свой список подсказок.

Q2: Что касается стратегий, руководство по Prover9 содержит полезную информацию. по взвешиванию, подсказкам и семантическому руководству (я не пробовал семантическое руководство). Вы также можете ознакомиться с страницей Боба Вероффа (часть его работы была выполнена в OTTER, но программы похожи). Также имеется полезная информация из записных книжек Ларри Воса, а также опубликованные работы доктора Воса, хотя все последние работы Воса получили сделано с помощью OTTER (опять же, программы похожи).

person Doug Spoonwood    schedule 13.06.2014