Почему некоторые механизмы вывода нуждаются в человеческой помощи, а другие нет?

^{Я сам изучаю Автоматизированное доказательство теорем / SMT-решатели / Помощники по проверке и выкладываю серию вопросов о процессе, начиная здесь .}

Почему автоматические средства проверки теорем, то есть ACL2 , и решатели SMT не нуждаются в помощи человека, в то время как помощники по доказательствам, то есть Изабель и Кок , нуждаются в помощи ?

^{Найти следующий вопрос серии здесь .}

Правильность формул более высокого порядка, как правило, не решаема, и пространства для поиска огромны , поэтому все, на что вы можете надеяться, - это пытаться найти доказательство - при условии, что оно существует - путем умного перечисления пространства для доказательства (например, кувалдой , удачно названной) но это грубо. Люди могут играть в оракула, предоставляя ключевые леммы для руководства доказательствами.

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

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

Малая азбука

• validity - формула valid, она содержит все, что вы присваиваете свободным переменным.
• $\forall$$\exists$
• decidability - (логическое) свойство (Turing) разрешимо, если существует алгоритм, который отвечает «да» или «нет» (правильно) по истечении определенного промежутка времени.
• логика высказываний - также логика нулевого порядка ; количественное определение не допускается.
• $\forall x. P(x)$$\forall f. f(4) > 0$
• логика высшего порядка - вы можете количественно определять (и «строить») произвольно сложные объекты, например функции высшего порядка (функции, которые принимают функции).

Я бы сказал, что классическое различие между «автоматическим доказательством теорем» (ATP) и «интерактивным доказательством теорем» (ITP) необходимо пересмотреть. Если сегодня взять хорошо известную систему ITP, такую ​​как Isabelle / HOL (Isabelle2013, февраль 2013 г.), она объединяет довольно много дополнительных инструментов из портфеля ATP:

• Встроенные универсальные автоматизированные средства проверки: инструменты старой школы Isabelle, такие как fastи blast(Л. Полсон), и более новые автоматизированные средства проверки, подобные metis(Дж. Херд).

• Внешние ATP для логики первого порядка, которые вызываются с помощью Sledgehammer: E prover, SPASS, Vampire. Найденное доказательство анализируется, чтобы выяснить, какие леммы внесли свой вклад, сократив 10000 до 10 с и подкрепив результат metis.

• Внешние SMT с частичной реконструкцией доказательства, особенно для Z3 (С. Беме).

• Инструменты для поиска встречных примеров недоказанных утверждений: Nitpick / Kodkodi (J. Blanchette) и Quickcheck (L. Bulwahn).

Делает ли все эти автоматизированные вещи Изабель автоматическим доказателем теорем?

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

В отличие от этого, система ITP создана для тех, кто ждет на месте с полуприличным доступом к внутренним состояниям доказательства, чтобы увидеть, чего не хватает, чтобы закончить доказательство. Система ITP, которая объединяет инструменты ATP в манере Изабель, может оказаться более привлекательной для большего количества пользователей и большего количества приложений, чем одна ITP или ATP.