Из теоремы Черча мы знаем, что определение выполнимости первого порядка вообще неразрешимо, но есть несколько методов, которые мы можем использовать для определения выполнимости первого порядка. Наиболее очевидным является поиск конечной модели. Однако в логике первого порядка есть ряд утверждений, которые, как мы можем продемонстрировать, не имеют конечных моделей. Например, любая область, в которой действует инъективная и не сюръективная функция, бесконечна.
Как мы можем продемонстрировать выполнимость для операторов первого порядка, где нет конечных моделей или существование конечных моделей неизвестно? В автоматическом доказательстве теорем мы можем определить выполнимость несколькими способами:
- Мы можем отрицать предложение и искать противоречие. Если он найден, мы доказываем правильность утверждения первого порядка и, следовательно, выполнимость.
- Мы используем насыщенность с разрешением и исчерпывающие выводы. Чаще всего у нас будет бесконечное количество выводов, поэтому это ненадежно.
- Мы можем использовать принуждение, которое предполагает существование модели, а также последовательность теории.
Я не знаю никого, кто бы применял форсирование как механизированную технику для автоматического доказательства теорем, и это выглядит нелегко, но мне интересно, было ли это сделано или предпринято, так как он использовался для доказательства независимости ряда утверждений в теории множеств, которая сама по себе не имеет конечных моделей.
Известны ли другие методы поиска соответствия первого порядка, применимые для автоматического рассуждения, или кто-то работал над алгоритмом автоматического форсирования?
Ответы:
Вот забавный подход Брока-Наннестада и Шюрмана:
Правдивые монадические абстракции
Идея состоит в том, чтобы попытаться перевести предложения первого порядка в монадическую логику первого порядка , «забыв» некоторые аргументы. Конечно, перевод не завершен : есть некоторые непротиворечивые предложения, которые становятся непоследовательными после перевода.
Однако монадическая логика первого порядка разрешима . Поэтому можно проверить, если переводF¯¯¯¯ формулы F согласуется:
может быть проверено процедурой принятия решения и подразумевает
Отсюда следует, что имеет модель по теореме полноты.F
Эта тема может применяться несколько в более общем смысле: определить разрешимую подлогику вашей проблемы, а затем перевести вашу проблему в нее таким образом, чтобы сохранить правду. В частности, современные SMT-решатели, такие как Z3, оказались удивительно хорошими в доказательстве выполнимости формул с квантификаторами (по умолчанию , но могут хорошо работать с формулами ).Σ01 Π02
В настоящее время форсирование, по-видимому, далеко недоступно для автоматизированных методов.
источник