Вопросы по теме 'theorem-proving'
Сопоставление с образцом без специализации типов
Я играю в Coq, пытаясь создать отсортированный список. Мне просто нужна функция, которая берет список [1,2,3,2,4] и возвращает что-то вроде Sorted [1,2,3,4] , т.е. удаляет плохие части, но не сортирует весь список.
Я подумал, что начну с...
1387 просмотров
schedule
13.03.2023
Как продолжить работу с этим Coq Proof?
У меня проблема с моим доказательством Coq, и я надеялся на некоторую помощь и руководство. У меня есть часть моего определения ниже:
Inductive Architecture : Set :=
| Create_Architecture (Arch_Name: string)(MyComponents: list Component)...
291 просмотров
schedule
26.07.2022
Завершить доказательство с ложной гипотезой в Coq
Итак, у меня есть ложная гипотеза в подцели. Это равенство между разными конструкторами. Как завершить подцель?
H: List.Not_Empty Bit.Bit Bit.Zero (List.Empty Bit.Bit) = List.Empty Bit.Bit
2062 просмотров
schedule
18.05.2022
Решение этого упражнения coq
Я изучаю COQ и застрял на одном из книжных упражнений. Книга не дает мне решения, поэтому я не знаю, что делать. Но я сделал первый. Я должен перевести эти утверждения в логику предикатов:
h0 : Everybody knows somebody
h1 : Nobody doesn't...
239 просмотров
schedule
29.06.2022
Coq: определение функции на основе теорем единственности и существования
Чтобы максимально изолировать эту проблему, предположим, что я начинаю сеанс Coq следующим образом.
Parameter A : Type.
Parameter B : Type.
Parameter P : A -> B -> Prop.
Axiom existence : forall a : A, exists b : B, P a b.
Axiom uniqueness...
596 просмотров
schedule
22.01.2023
Z3: выполнение матричных операций
Моя ситуация
Я работаю над проектом, который должен:
Докажите правильность формул преобразования трехмерных матриц , включающих матричные операции.
Найдите модель со значениями неизвестных элементов матрицы.
Мой вопрос
Как лучше всего...
1497 просмотров
schedule
26.07.2023
Что доказывает лемма perm_invK в Ssreflect?
Следующий код взят из perm.v библиотеки Ssreflect Coq. Я хочу знать, что это за результат.
Lemma perm_invK s : cancel (fun x => iinv (perm_onto s x)) s.
Proof. by move=> x /=; rewrite f_iinv. Qed.
120 просмотров
schedule
14.07.2022
Coq не может найти подтермин при использовании тактики перезаписи
Я пытаюсь выполнить модифицированное подтверждение compile_correct из первой главы документа Certified Программирование с зависимыми типами. В своей версии я пытаюсь использовать тот факт, что progDenote является складкой, и использую более...
1461 просмотров
schedule
11.10.2022
Изабель - Нитпик - автоматическое использование значений свидетелей
Как я могу автоматически использовать значения, найденные nitpick , вместо того, чтобы использовать rule exI и вручную вводить значения свидетелей?
theorem "EX a b. a + b = 5 & a - b = (1 :: int)"
nitpick [falsify=false]
(*...
64 просмотров
schedule
27.11.2022
Докажите, что f(n) = Θ(g(n)) тогда и только тогда, когда g(n) = Θ(f(n))
Мне поставили задачу:
f(n) are asymptotically positive functions. Prove f(n) = Θ(g(n)) iff g(n) = Θ(f(n)).
Все, что я нашел, указывает на то, что это утверждение недействительно. Например, ответ, с которым я столкнулся, гласит:
f(n) =...
10970 просмотров
schedule
30.03.2023
Разница между логическим программированием и автоматическим доказательством теорем
В чем разница между логическим программированием и автоматическим доказательством теорем (ATP) (например, с помощью E-Prover, Spass или Princess)?
Я много искал, и единственная информация, которую я нашел, это то, что АТФ является предшественником...
586 просмотров
schedule
12.07.2022
набор интегрируемых с функцией умножения
Я пытаюсь доказать эту лемму:
lemma set_integral_mult:
fixes f g :: "_ ⇒ _ :: {banach, second_countable_topology}"
assumes "set_integrable M A (λx. f x)" "set_integrable M A (λx. g x)"
shows "set_integrable M A (λx. f x * g x)"
и...
88 просмотров
schedule
31.07.2023
Идрис Дек против Может быть
Какие вещи можно выразить с помощью Dec , а не с помощью Maybe в Идрисе ?
Или другими словами: когда следует выбирать Dec и когда Maybe ?
364 просмотров
schedule
11.01.2023
два поля записывают соответствие в Agda
Я хотел бы написать лимит в категории наборов, используя Agda . Предполагая локальную малость, функтор — это пара отображения на Set OC и I, как здесь.
sobj : OC → Set c₂
smap : { i j : OC } → (f : I ) → sobj i → sobj j
Конус для...
150 просмотров
schedule
12.03.2023
Как определить переводчик выражений?
Я определил 2 почти идентичных языка (foo и bar):
theory SimpTr
imports Main
begin
type_synonym vname = "string"
type_synonym 'a env = "vname ⇒ 'a option"
datatype foo_exp =
FooBConst bool |
FooIConst int |
FooLet vname foo_exp foo_exp...
59 просмотров
schedule
29.07.2023
Что означают ошибки типа !=‹ в agda и как их исправить
Я не могу найти информацию об этом на http://agda.readthedocs.io/en/v2.5.3/ , ни в книге "Проверенное программирование в agda". Что это значит? И где я могу узнать больше, как эта ошибка?
Полная ошибка .cter !=< cter of type Set
Код...
88 просмотров
schedule
05.07.2022
Как доказать, что свойство отношения выполняется для транзитивного замыкания этого отношения?
Я определил следующее свойство отношения:
definition rel_limited_under :: "('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool" where
"rel_limited_under R A =
(∀x y z :: 'a. R x y ⟶ R y z ⟶ x ∈ A ⟶ z ∈ A ⟶ y ∈ A)"
Отношение R ограничено множеством A...
92 просмотров
schedule
07.03.2023
Вопрос об использовании разрешения для поиска опровержения некоторых положений
Я делаю домашнюю работу по курсу искусственного интеллекта, и в настоящее время я застрял на вопросе о том, как найти опровержение некоторых пунктов.
Я перепробовал множество способов найти опровержение этих пунктов, однако в итоге он либо пришел к...
102 просмотров
schedule
26.07.2023
Простые доказательства равенства в списках в idris (доказательство xs++[x]=ys++[y]->x=y->xs=ys)
Я изучаю idris и очень заинтересован в доказательстве свойств списков.
Если вы посмотрите на стандартная библиотека , есть доказательство того, что "Два списка равны, если их головы и хвосты равны".
consCong2 : {x : a} -> {xs : List a}...
86 просмотров
schedule
04.06.2022
Доказательство ложного случая тогда и только тогда, когда в Агде
Я пытаюсь понять, как создать рабочий оператор «если и только если» в agda, но у меня проблемы с доказательством его ложных случаев, а также с использованием индукции в доказательстве. В качестве примера я хочу работать с «меньше или равно», которое...
209 просмотров
schedule
28.04.2022
