Логическое рассуждение и автоматическое доказательство теорем

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

Definition

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

Scope

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

Core questions

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

Key concepts

• пропозициональная логика и логика первого порядка
• следование и валидность
• унификация
• резолюция и опровержение
• DPLL и решение SAT
• прямой и обратный вывод
• хорновские дизъюнкты и логическое программирование
• корректность и полнота

Key theories

Принцип резолюции

Резолюция Робинсона — это единое правило вывода для дизъюнктов, которое в сочетании с унификацией является полным по опровержению для логики первого порядка: любая невыполнимая система дизъюнктов может быть показана невыполнимой путем вывода пустого дизъюнкта.

DPLL и пропозициональная выполнимость

Процедура Дэвиса-Патнэма и ее усовершенствование DPLL определяют пропозициональную выполнимость путем систематического разбиения случаев с распространением единичных дизъюнктов и исключением чистых литералов, формируя основу современных SAT-решателей.

Логическое программирование и обратный вывод

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

Clinical relevance

Автоматическое доказательство теорем и решение SAT/SMT используются при верификации аппаратного и программного обеспечения, анализе программ, планировании и математике, в то время как языки логического программирования, такие как Prolog, применяют вывод с обратной цепочкой к базам данных, синтаксическому анализу и системам, основанным на правилах.

History

Ранние процедуры доказательства, разработанные Гилмором, Дэвисом и Патнэмом (1960), автоматизировали пропозициональные и кванторные рассуждения, а принцип резолюции Робинсона (1965) объединил вывод первого порядка в одно правило. В 1970-х годах резолюция была усовершенствована в логическое программирование и Prolog; позднее решение SAT и SMT превратилось в важную практическую технологию.

Key figures

• John Alan Robinson
• Martin Davis
• Hilary Putnam
• Robert Kowalski
• Alan Robinson

Seminal works

• robinson1965
• davis1960
• kowalski1979

Frequently asked questions

Что такое принцип резолюции?

Резолюция — это единое правило вывода, которое принимает два дизъюнкта, содержащие комплементарные литералы, и производит новый дизъюнкт, объединяющий остальные. Применяемая многократно с унификацией, она может показать, что набор дизъюнктов первого порядка невыполним, что является основой для доказательства теорем методом опровержения.

Гарантировано ли завершение автоматического доказательства теорем?

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