Вопросы по теме 'theorem-proving'
Изабель: транспонировать матрицу, включающую постоянный множитель
В моей теории Изабель у меня есть матрица с постоянным множителем:
...
k :: 'n and c :: 'a
(χ i j. if j = k then c * (A $ i $ j) else A $ i $ j)
Я могу вычислить транспонированную матрицу:
(transpose (χ i j. if j = k then c * (A $ i $ j)...
203 просмотров
schedule
30.08.2023
Подсказки Prover9 не используются
Я запускаю некоторые доказательства решетки через Prover9/Mace4. Я использую нестандартную аксиоматизацию операции решеточного соединения, из которой сразу не следует, что соединение является коммутативным, ассоциативным и идемпотентным. (Я могу...
330 просмотров
schedule
05.05.2024
Расширение рекурсивных функций в Coq
Фон
Я понимаю, что редукция Йота используется для уменьшения/расширения рекурсивных функций. Например, при следующем применении простой рекурсивной функции (факториал над натуральными числами):
((fix fact (n:nat):nat := match n with | O =>...
490 просмотров
schedule
05.01.2023
Поведение применяемой тактики, когда цель и применяемый термин совпадают
Предположим, у нас есть A B C : Prop . Учитывая контекст с H : A -> B -> C и единственной целью A -> B -> C , почему можно apply H завершить доказательство, решив текущую и единственную цель?
Я думал, что тактика apply...
57 просмотров
schedule
16.11.2022
Использование существующего определения в Isabelle / Hol
Я новый пользователь Isabelle / Hol, и у меня есть некоторая путаница относительно использования существующих определений в Isabelle. Мне нужно определить структуру полной решетки и структуру полного частичного порядка (CPO) в моей модели. Я...
133 просмотров
schedule
28.11.2022
Почему simp не может применить метод начального доказательства, когда взрыв успешно работает с теми же фактами?
Я смоделировал это исчисление в Изабель в качестве упражнения. Вот мой код на данный момент.
Я использую кувалду для доказательства простых теорем, которые обычно предлагают использовать взрыв, дополненный подмножеством правил исчисления,...
372 просмотров
schedule
25.05.2022
Что составляет действительный тип бережливого производства?
Я прочитал первые 3 главы руководства по бережливому производству и уже сделал несколько доказательств в логике высказываний .
Теперь я пытаюсь немного вернуться назад и задавать себе глупые вопросы .
Я так понимаю:
Термины могут иметь...
83 просмотров
schedule
13.01.2024
Coq не генерирует индуктивную гипотезу
Мне дали решение следующей теоремы, как показано ниже:
Require Import Coq.Lists.List.
Import ListNotations.
Inductive suffix {X : Type} : list X -> list X -> Prop :=
| suffix_end : forall xs,
suffix xs xs
| suffix_step :...
144 просмотров
schedule
20.03.2022
Как сопоставить с образцом на опоре при испытании в Coq без исключения на Type
Я пытаюсь доказать, что хвост отсортированного списка сортируется в Coq, используя сопоставление с образцом вместо тактики:
Require Import Coq.Sorting.Sorted.
Definition tail_also_sorted {A : Prop} {R : relation A} {h : A} {t : list A}...
514 просмотров
schedule
04.05.2022
Есть ли в Isabelle аддитивная версия Power.thy?
В Изабель я определил функцию f:'a -> nat , где 'a - некоторая алгебраическая структура, которая расширяет моноид (то есть группу, полукольцо, кольцо, область целостности, поле, ...).
Я хотел бы использовать вывод этой функции как...
38 просмотров
schedule
26.05.2022
Ltac: делайте что-то другое в каждой цели
У меня есть сценарий проверки, в котором я исследую несколько случаев, и в настоящее время он довольно медленный, поскольку у меня есть несколько стратегий для решения целей, и я пробую каждую из них в каждом случае.
Я знаю, что мне нужно применять...
217 просмотров
schedule
12.10.2023
перезапись не изменила ошибку типа для визуально одинаковых типов
Я написал короткую функцию:
swapMaybe : Monad m => Maybe (m a) -> m (Maybe a)
swapMaybe Nothing = pure Nothing
swapMaybe (Just x) = map Just x
Затем я попытался доказать одно из его свойств:
import Interfaces.Verified...
69 просмотров
schedule
21.02.2022
Шаблон умного конструктора во время испытаний с Изабель
Изучая главу 3 Concrete Semantics , мой инструктор заметил, что некоторые функции были построены с использованием шаблона интеллектуального конструктора и заявили, что этот шаблон полезен для доказательства теорем.
Я искал в Google умные...
50 просмотров
schedule
12.05.2022
Как убрать скобки в алгебраических выражениях с помощью Lean
Я пытаюсь доказать одну алгебраическую теорему, используя Lean. Мой код
import algebra.group
import algebra.ring
open algebra
variable {A : Type}
variables [s : ring A] (a b c : A)
include s
theorem clown (a b c d e : A) :
(a + b + e) * ( c...
148 просмотров
schedule
02.09.2022
Изабель 2017 начало работы
Я пытаюсь научиться использовать Isabelle / HOL. Я подумал: «Эй, учебник, написанный некоторыми людьми, которые его разработали, было бы здорово», и поэтому посмотрел на https://isabelle.in.tum.de/doc/tutorial.pdf , дата публикации которого - 15...
408 просмотров
schedule
25.11.2023
Prover9 Некоторые, но не все запрошенные доказательства были найдены
Я запускаю некоторые доказательства решетки через Prover9/Mace4. Prover9 говорит Exit: Time limit. плюс сообщение в Заголовке.
Я удвоил лимит времени с 60 до 120 секунд. То же сообщение (в два раза быстрее). Странно вот что:
есть только...
321 просмотров
schedule
23.07.2023
Проверить теорему свертки с помощью pytorch
В основном эта теорема формулируется следующим образом:
F(f*g) = F(f)xF(g)
Я знаю эту теорему, но я просто не могу воспроизвести результат с помощью pytorch.
Ниже приведен воспроизводимый код:
import torch
import torch.nn.functional as...
747 просмотров
schedule
29.06.2023
Есть ли в Изабель тактика переписывания?
Например, в Coq есть rewrite , и мы также можем поставить стрелки `‹ -:
Inductive bool: Set :=
| true
| false.
Lemma equality_of_functions_commutes:
forall (f: bool->bool) x y,
(f x) = (f y) -> (f y) = (f x).
Proof.
intros....
128 просмотров
schedule
04.02.2022
Идрис передает функции доказательство того, что аргументы являются LTE
У меня есть функция, которая вычитает два Nat . Как мне доказать, что первый аргумент, который я ему передаю, на самом деле меньше второго?
dummy : (k : Nat) -> (n : Nat) -> {auto smaller : LTE k n} -> Nat
dummy k n = n - k
Я...
63 просмотров
schedule
14.10.2023
API для стратегий доказательства теорем
Существуют ли высокоуровневые API/среды/библиотеки для проверки эффективности конкретного подхода (например, эвристического алгоритма) для создания конструктивных доказательств на основе логики первого порядка/теории типов?
Я пытаюсь найти удобный...
122 просмотров
schedule
30.11.2022
