Вопросы с тегом «automated-theorem-proving»

Автоматическое доказательство теорем - это доказательство математических теорем с помощью компьютерной программы.

35
Если P = NP, можем ли мы получить доказательства гипотезы Гольдбаха и т. Д.?

Это наивный вопрос, из моего опыта; заранее извиняюсь. Гипотеза Гольдбаха и многие другие нерешенные вопросы математики могут быть записаны в виде кратких формул в исчислении предикатов. Например, статья Кука "Могут ли компьютеры регулярно находить математические доказательства?" формулирует эту...

28
Существует ли разумная автоматизированная система доказательств для теорем TCS?

Предположим, я хотел формализовать доказательство Тьюринга относительно проблемы остановки, чтобы машина могла его проверить. Некоторые из известных автоматизированных систем доказательства теорем включают Mizar, Coq и HOL4. Я скачал и экспериментировал с Coq, но у него нет библиотеки для машин...

18
Почему компьютеру так сложно что-то доказать?

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

18
Автоматическое доказательство теорем в линейной логике

Является ли автоматическое доказательство теорем и поиск доказательств более простым в линейных и других пропозициональных субструктурных логиках, в которых отсутствует сжатие? Где я могу прочитать больше об автоматическом доказательстве теорем в этих логиках и роли сокращения в поиске...

15
Как определить, требует ли доказательство «методов рассуждения более высокого порядка»?

Вопрос: Предположим, у меня есть спецификация задачи, состоящей из аксиом и цели (т. Е. Связанная проблема доказательства состоит в том, является ли цель выполнимой при всех аксиомах). Предположим также, что проблема не содержит каких-либо противоречий / противоречий между аксиомами. Есть ли способ...

14
Логические соотношения для предиктивной системы в предикативной мета-теории

Логические отношения для непредсказуемых языков, таких как Система F, похоже, критически полагаются на непредсказуемость внешней логики. В частности, интерпретация для типа Форалла будет определяться в терминах всех типизированных отношений. В непредсказуемой системе (например, CiC / Coq) это...

13
Каковы практически вычислимые свойства маркированных систем переходов?

Я обнаружил, что маркированные переходные системы являются хорошей моделью для моего приложения, а именно есть статья о моделировании вариантов использования с использованием LTS. Вопрос в том, что можно легко доказать о LTS? Я хотел бы повторно использовать существующие решения, чтобы увидеть,...

11
Доказательства найдены на компьютере

В 1996 году давно открытая проблема была решена с помощью компьютера; а именно, что алгебра Роббинса и булева алгебра совпадают. Доказательство было найдено автоматическим испытателем теорем. Кроме того, известное доказательство теоремы о четырех цветах содержит сгенерированные компьютером...

11
Какая парадигма автоматического доказательства теорем подходит для формализации в стиле Principia Mathematica?

У меня есть книга, которая, вдохновленная Принципами математики Рассела (PM) и логическим позитивизмом, пытается формализовать определенную область, определяя аксиомы и выводя из них теоремы. Короче говоря, он пытается сделать для своей области то, что PM пытался сделать для математики. Как и PM,...

11
Состояние искусства для монадического класса?

В монадической логике первого порядка, также известной как монадический класс задачи решения, все предикаты принимают один аргумент. Аккерманн показал, что он может быть разрешен и НЕОБХОДИМО завершен . Однако такие проблемы, как SAT и SMT, имеют быстрые алгоритмы их решения, несмотря на...

10
Существуют ли процедуры полу-решения для этой теории?

У меня есть следующая типизированная теория |- 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...

9
Выполнимость первого порядка, которая не имеет конечных моделей

Из теоремы Черча мы знаем, что определение выполнимости первого порядка вообще неразрешимо, но есть несколько методов, которые мы можем использовать для определения выполнимости первого порядка. Наиболее очевидным является поиск конечной модели. Однако в логике первого порядка есть ряд утверждений,...

9
Почему проверка кода требуется в коде переноса доказательства

В классической статье PLDI'98 Necula «Разработка и реализация сертифицирующего компилятора» верификатор высокого уровня использует: VCGen для генерации условий проверки (предикаты безопасности) Доказательство логической теоремы первого порядка для доказательства условий LF proof checker для...