Автоматическое доказательство теорем - это доказательство математических теорем с помощью компьютерной программы.
Это наивный вопрос, из моего опыта; заранее извиняюсь. Гипотеза Гольдбаха и многие другие нерешенные вопросы математики могут быть записаны в виде кратких формул в исчислении предикатов. Например, статья Кука "Могут ли компьютеры регулярно находить математические доказательства?" формулирует эту...
Предположим, я хотел формализовать доказательство Тьюринга относительно проблемы остановки, чтобы машина могла его проверить. Некоторые из известных автоматизированных систем доказательства теорем включают Mizar, Coq и HOL4. Я скачал и экспериментировал с Coq, но у него нет библиотеки для машин...
Это можно считать глупым вопросом. Я не специализируюсь в области компьютерных наук (и еще не изучаю математику), поэтому, пожалуйста, извините, если вы считаете, что следующие вопросы отражают некоторые ошибочные предположения. Хотя есть планы формализовать последнюю теорему Ферма (см. Эту...
Является ли автоматическое доказательство теорем и поиск доказательств более простым в линейных и других пропозициональных субструктурных логиках, в которых отсутствует сжатие? Где я могу прочитать больше об автоматическом доказательстве теорем в этих логиках и роли сокращения в поиске...
Вопрос: Предположим, у меня есть спецификация задачи, состоящей из аксиом и цели (т. Е. Связанная проблема доказательства состоит в том, является ли цель выполнимой при всех аксиомах). Предположим также, что проблема не содержит каких-либо противоречий / противоречий между аксиомами. Есть ли способ...
Логические отношения для непредсказуемых языков, таких как Система F, похоже, критически полагаются на непредсказуемость внешней логики. В частности, интерпретация для типа Форалла будет определяться в терминах всех типизированных отношений. В непредсказуемой системе (например, CiC / Coq) это...
Я обнаружил, что маркированные переходные системы являются хорошей моделью для моего приложения, а именно есть статья о моделировании вариантов использования с использованием LTS. Вопрос в том, что можно легко доказать о LTS? Я хотел бы повторно использовать существующие решения, чтобы увидеть,...
В 1996 году давно открытая проблема была решена с помощью компьютера; а именно, что алгебра Роббинса и булева алгебра совпадают. Доказательство было найдено автоматическим испытателем теорем. Кроме того, известное доказательство теоремы о четырех цветах содержит сгенерированные компьютером...
У меня есть книга, которая, вдохновленная Принципами математики Рассела (PM) и логическим позитивизмом, пытается формализовать определенную область, определяя аксиомы и выводя из них теоремы. Короче говоря, он пытается сделать для своей области то, что PM пытался сделать для математики. Как и PM,...
В монадической логике первого порядка, также известной как монадический класс задачи решения, все предикаты принимают один аргумент. Аккерманн показал, что он может быть разрешен и НЕОБХОДИМО завершен . Однако такие проблемы, как SAT и SMT, имеют быстрые алгоритмы их решения, несмотря на...
У меня есть следующая типизированная теория |- 1_X : X -> X f : A -> B, g : B -> C |- compose(g,f) : A -> C F, f : A -> B |- apply(F,f) : F(A) -> F(B) с уравнениями для всех членов: f : A -> B, g : B -> C, h : C -> D |- compose(h,compose(f,g)) = compose(compose(h,f),g) f...
Из теоремы Черча мы знаем, что определение выполнимости первого порядка вообще неразрешимо, но есть несколько методов, которые мы можем использовать для определения выполнимости первого порядка. Наиболее очевидным является поиск конечной модели. Однако в логике первого порядка есть ряд утверждений,...
В классической статье PLDI'98 Necula «Разработка и реализация сертифицирующего компилятора» верификатор высокого уровня использует: VCGen для генерации условий проверки (предикаты безопасности) Доказательство логической теоремы первого порядка для доказательства условий LF proof checker для...