Описание тега theorem-proving

Описание тега Вопросы с тегом
Доказательство теорем, в настоящее время наиболее развитая область автоматизированных рассуждений, - это доказательство математических теорем с помощью компьютерной программы.
1 ответ

Матричная арифметика Изабель: det_linear_row_setsum в библиотеке с другой системой обозначений

Недавно я начал использовать доказатель теоремы Изабель. Поскольку я хочу доказать другую лемму, я хотел бы использовать нотацию, отличную от той, которая используется в лемме "det_linear_row_setsum", которую можно найти в библиотеке HOL. Более конк…
25 июн '13 в 14:08
0 ответов

Восстановление лямбд в Coq без равенства экстенсиональных функций?

Я перейду к основам программного обеспечения. Есть два определения данной функции обратного списка. Fixpoint rev (l:natlist) : natlist := match l with | nil => nil | h :: t => rev t ++ [h] end. и хвост-рекурсивный: Fixpoint rev_append {X} (l1 …
07 окт '16 в 08:15
1 ответ

Умный образец конструктора во время прувинга с Изабель

Во время изучения главы 3 " Конкретная семантика" мой инструктор упомянул, что некоторые функции были построены с использованием шаблона "умный конструктор", и заявил, что этот шаблон полезен для доказательства теорем. Я гуглил умных конструкторов, …
23 окт '18 в 15:32
1 ответ

Нормальное определение константы в сравнении с определением лямбда-константы

У меня есть эти два определения. Почему они разворачиваются по-разному? Как я могу доказать леммы о "ой"? (И вообще, в чем разница между этими двумя определениями в Изабель, внутри?) (Пожалуйста, не направляйте меня на внешние ссылки, потому что я о…
24 окт '15 в 17:49
0 ответов

Нужна помощь в создании мини-проекта, основанного на автоматическом доказательстве теорем с использованием языка Си

Я четвертый курс бакалавра компьютерных наук и инженерии, и наша команда работает над мини-проектом по автоматическому доказательству теорем. Наша главная цель - выяснить, является ли геометрическая теорема действительной или нет, основываясь на акс…
04 апр '17 в 06:56
2 ответа

Как определить частично упорядоченные множества в Lean?

Я хочу доказать эту теорему в доказательстве теоремы Лин. Во-первых, мне нужно определить такие вещи, как частично упорядоченные множества, чтобы я мог определить infimum / supremum. Как это делается в Lean? В учебнике упоминаются сетоиды, которые я…
27 мар '16 в 18:48
0 ответов

Простой тест Prover9 не работает

У меня есть файл, который я использую в качестве входных данных для доказательства теоремы9. Он содержит только предположения. Я решил протестировать Prover9, используя в качестве цели одно из предположений. Очевидно, это должно быть доказано. Тем н…
04 апр '18 в 12:02
1 ответ

Использование массива в Z3PY

Я использую z3 для своего исследования, и у меня есть следующая проблема. Я анализирую модель выполнимой формулы, которая содержит массивы, но я не понимаю результатов модели. Например, у меня есть две переменные 'pkgcounter' и 'rxlen' и два предлож…
19 июл '16 в 13:53
1 ответ

Заявить-весело и определить-весело в Z3 не может работать вместе?

Мне нужно смоделировать длину массива. Поэтому я объявляю функцию (declare-fun LEN ((Array Int Int)) Int) В то же время я хочу определить некоторые макросы, используя define-fun, Однако, как я немного протестировал на Z3, кажется, что define-fun а т…
04 дек '12 в 05:39
0 ответов

Доказательство теоремы с доказательством 9 - противоречивый результат

Я использую Prover9 для доказательства теорем первого порядка, с интерфейсом Python nltk. Я получаю разные результаты для двух эквивалентных формул (без предположений):Пусть р1: -exists x0.(-exists x3 x1.(R0(x3,x0) & R0(x1,x1)) & exists x1 x…
14 окт '18 в 08:41
1 ответ

Печать внутренних решающих формул в z3

Инструмент доказательства теорем z3 занимает много времени, чтобы решить формулу, с которой, я думаю, она сможет легко справиться. Чтобы лучше понять это и, возможно, оптимизировать мой ввод в z3, я хотел увидеть внутренние ограничения, которые z3 г…
27 окт '12 в 18:09
1 ответ

Знание, когда доказательство в стиле Изара действительно в Изабель

Я работаю над упражнением, пытаясь выучить язык изар. У меня есть следующий скрипт для леммы о списках. lemma "EX ys zs. xs = ys @ zs ∧ (length ys = length zs ∨ length ys = length zs + 1)" proof - show ?thesis by blast (* L *) qed Кажется, Изабель п…
11 янв '19 в 22:56
2 ответа

Сильная индукция в списках

Я пытаюсь доказать, что предложение P выполняется для каждого элемента типа A, К сожалению, я знаю только как доказать P для данного a:A если у меня есть доступ к доказательствам P для всех a' меньше, чем a, Это должно быть доказано введением в спис…
01 фев '16 в 03:30
1 ответ

Сокращение количества используемых предложений с использованием цели доказательства в Z3

Я экспериментирую с оптимизацией использования Z3 для доказательства фактов о теории первого порядка. В настоящее время я задаю теорию первого порядка в Python, обосновываю квантификаторы и отправляю все предложения вместе с отрицанием цели доказате…
21 дек '12 в 20:49
3 ответа

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

Я ищу автоматическую систему доказательства теорем, которая может доказать это: Крокодил взял мужик ребенка. Человек попросил крокодила не есть его ребенка. Но Крокодил сказал: я верну тебе твоего ребенка, если ты скажешь мне, что я собираюсь делать…
25 июн '13 в 14:27
1 ответ

От включения набора для установления равенства в Lean

Учитывая доказательство включения множества и его обратное, я хотел бы показать, что два множества равны. Например, я знаю, как доказать следующее утверждение и его обратное утверждение: open set universe u variable elem_type : Type u variable A : s…
13 авг '17 в 09:28
2 ответа

Как я могу доказать, что тип действителен в Agda?

Я пытаюсь сделать доказательства по зависимым функциям, и я сталкиваюсь с загадкой. Итак, скажем, у нас есть теорема F-равно f-equal : ∀ {A B} {f : A → B} {x y : A} → x ≡ y → f x ≡ f y f-equal refl = refl Я пытаюсь доказать более общее представление…
09 сен '14 в 06:01
1 ответ

Нужна помощь в понимании метода Овики-Гриза

Я (по ошибке) взял курс о проверке параллельных программ, и мы до сих пор рассматривали этот метод, называемый "метод Овики-Гриза". По-видимому, можно доказать различные результаты о программе, связав утверждение с каждым утверждением, и показать, ч…
25 сен '14 в 05:15
2 ответа

SMT решатели для битовой векторной арифметики

Я планирую несколько экспериментов по символическому исполнению кода на языке C, используя готовый SMT-решатель, и задаюсь вопросом, какой решатель использовать; например, рассматривая участников конкурса SMT и принимая только системы с открытым исх…
07 июн '11 в 10:33
1 ответ

Coq: признать, отстаивать

Есть ли способ признать утверждения в Coq? Предположим, у меня есть такая теорема: Theorem test : forall m n : nat, m * n = n * m. Proof. intros n m. assert (H1: m + m * n = m * S n). { Admitted. } Abort. Вышеупомянутое утверждение, кажется, не рабо…
14 мар '17 в 16:28