Вопросы по теме 'theorem-proving'
Аксиомы комбинаторной логики
Я провожу некоторые эксперименты по доказательству теорем с помощью комбинаторной логики, что выглядит многообещающе, но есть один камень преткновения: было указано, что в комбинаторной логике верно, что, например, I = SKK, но это не теорема, это...
743 просмотров
schedule
31.12.2022
Ограничения решателей SMT
Традиционно большая часть работы с вычислительной логикой была либо пропозициональной, и в этом случае вы использовали решатель SAT (булева выполнимость), либо первым порядком, и в этом случае вы использовали средство доказательства теорем первого...
4211 просмотров
schedule
23.10.2022
Используя экзистенциальную теорему в Coq
У меня есть следующая теорема в Coq: Theorem T : exists x:A, P x. Я хочу иметь возможность использовать это значение в последующем доказательстве. I.E. Я хочу сказать что-то вроде: «пусть o представляет такое значение, что P o . Я знаю, что o...
521 просмотров
schedule
10.08.2022
Как сделать нотации видимыми вне подписи модуля в Coq?
Я определил сигнатуру модуля в Coq, которая определяет несколько обозначений. Однако, когда я пытаюсь использовать эти обозначения вне подписи, Coq терпит неудачу. Упрощенная версия моего кода приведена ниже. Любая помощь будет оценена по...
340 просмотров
schedule
12.05.2023
Coq: проблемы со списком в индуктивном
Я новичок в Coq, но с некоторыми усилиями мне удалось доказать различные индуктивные леммы. Однако я застреваю на всех упражнениях, в которых используется следующее индуктивное определение:
Inductive In (A:Type) (y:A) : list A -> Prop :=...
1260 просмотров
schedule
30.05.2023
Изабель: Кувалда находит доказательство, но оно не работает
Часто у меня возникает проблема, что sledgehammer находит доказательство, но когда я вставляю его, оно не прекращается. Думаю, sledgehammer - одна из самых важных частей Изабель, но потом это начинает раздражать, если доказательство не удается....
1685 просмотров
schedule
30.03.2022
Средство доказательства геометрических теорем с поддержкой пересечения квадратов
Я пытаюсь автоматически доказать/опровергнуть некоторые теоремы геометрии, связанные с квадратами, такие как «Для каждых 3 наборов из 7 непересекающихся квадратов можно выбрать 1 квадрат из каждого набора, так что 3 представителя являются внутренними...
172 просмотров
schedule
07.09.2022
Определение монады Maybe в Coq
Я хочу определить монаду Maybe, используя класс типов в Coq. Monad наследует Functor .
Я хочу доказать Some (f x') = fmap f (Some x') , который является одним из законов монад. Я использовал compute , reflexivity и destruct option_functor...
822 просмотров
schedule
14.05.2023
Возможная ошибка с Z3: Z3 не может доказать теорему в топологии
Я пытаюсь доказать с помощью Z3 теорему общей топологии, изложенную в
Топология TPTP
Я перевожу приведенный там код, используя следующий код Z3-SMT-LIB
;; File : TOP001-2 : TPTP v6.0.0. Released v1.0.0.
;; Domain : Topology
;;...
149 просмотров
schedule
07.07.2022
Пользовательская тактика прувера в Идрисе
Если я правильно понимаю (в основном из-за наличия функции applyTactic ), то можно написать собственную тактику для доказателя теорем в Идрисе. Какие (или где) примеры я мог бы использовать, чтобы узнать, как это сделать?
726 просмотров
schedule
03.08.2022
Функция получения сортировки с 2-мя параметрами в конструкторе
Я создал 4 вида (Task, Role, User и Run), последний получает 2 параметра, затем я объявляю забаву для каждого из них, в том числе один для Run , вызываю P, который получает 2 параметра для создания «экземпляра» Run . Затем я создал два массива, один...
100 просмотров
schedule
03.05.2023
Как описать отношения "один-много" в Coq?
Я читал книгу Б. Рассела «Введение в математическую философию» и пытался формализовать все описанные в ней теоремы.
Отношения "один-много" описываются следующим текстом ( контексты в книге ).
Отношения «один-много» можно определить как...
220 просмотров
schedule
14.09.2022
Как я могу подтвердить, что тип действителен в Agda?
Я пытаюсь провести доказательства по зависимым функциям, и у меня возникла загвоздка.
Итак, допустим, у нас есть теорема f-equal
f-equal : ∀ {A B} {f : A → B} {x y : A} → x ≡ y → f x ≡ f y
f-equal refl = refl
Я пытаюсь доказать более общее...
326 просмотров
schedule
17.12.2022
Доказательство теорем / помощник по доказательству, поддерживающий (множественные) подтипы / подклассы
Короче говоря, я ищу средство доказательства теорем, основная логика которого поддерживает механизм множественного подтипа/подкласса. (Я пытался использовать Isabelle, но, похоже, он не обеспечивает первоклассную поддержку подтипа. см. это )
Я...
340 просмотров
schedule
03.07.2022
нужно определение в Изабель, чтобы показать, что две частичные функции никогда не производят одинаковый результат
Я использую математический инструментарий HOL-Z для выполнения некоторых предикатов Изабель. в частности, я использую частичное определение функции для определения некоторых отношений в спецификации Z, которую я пишу, где я конвертирую схему в...
186 просмотров
schedule
14.04.2022
Агда: формирование всех пар {(x, y) | х в хс, у в ys}
Мне интересно, как лучше всего подойти к спискам или декартовым продуктам в Agda.
У меня есть два вектора, xs и ys . Я хочу (неформальный) набор {(x, y) | x в xs, y в ys }.
Я могу довольно легко сформировать этот набор, используя map и...
246 просмотров
schedule
14.09.2022
Z3 Java API - получить ядро unsat
Я пытаюсь понять, как получить ядро unsat с помощью Java API для Z3. Наш сценарий выглядит следующим образом (внизу код, который работает в rise4fun):
Создаем вход SMT2 программно
Входные данные содержат определения функций, объявления типов...
540 просмотров
schedule
26.12.2021
Haskell - используйте индукцию, чтобы доказать импликацию
Я должен доказать по индукции, что
no f xs ==> null (filter f xs)
Где :
filter p [] = []
filter p (x:xs)
| p x = x : filter p xs
| otherwise = filter p xs
null [] = True; null _ = False
no p [] = True
no p (x:xs)
|...
531 просмотров
schedule
15.04.2024
Как реализовать алгоритм Флойда заяц и черепаху в Agda?
Я хочу перевести следующий код Haskell в Agda:
import Control.Arrow (first)
import Control.Monad (join)
safeTail :: [a] -> [a]
safeTail [] = []
safeTail (_:xs) = xs
floyd :: [a] -> [a] -> ([a], [a])
floyd xs [] = ([], xs)...
251 просмотров
schedule
14.09.2023
Как определить частично упорядоченные наборы в Lean?
Я хочу доказать эту теорему с помощью средства доказательства теорем Lean. Во-первых, мне нужно определить такие вещи, как частично упорядоченные множества, чтобы я мог определить точную / верхнюю грань. Как это делается в Lean? В руководстве...
333 просмотров
schedule
28.05.2023
