Isar имеет, помимо assume , также команду presume для введения фактов в блок доказательства Isar. Из того, что я вижу и читаю в документации, это не требует, чтобы предположение (презумпция?) Было явно указано в цели, и, кажется, добавляет случай,...

Большинство помощников по доказательству - это функциональные языки программирования с зависимыми типами. Они могут проверять программы / алгоритмы. Вместо этого меня интересует помощник по доказательству, который лучше всего подходит для математики...

Скажем, я хочу доказать лемму ∃ n m k . [n, m, k] = [2, 3, 5] в Изабель / Изар. Если я продолжу, как предложено в учебнике Isabelle / HOL на странице 45, мое доказательство будет выглядеть следующим образом: lemma "∃ n m k . [n, m, k] = [2, 3,...

Предположим, у меня есть следующий код в Isabelle: typedecl type1 typedecl type2 typedecl type3 consts A::"type1 set" B::"type2 set" Когда я хочу использовать операцию объединения с A и B, как показано ниже: axiomatization where...

Я заинтересован в использовании Isar в качестве метаязыка для написания формальных доказательств J , исполняемого файла математические обозначения и язык программирования, и я хотел бы иметь возможность использовать J в качестве внутреннего...

Я пытаюсь использовать правило linordered_field_class.frac_le в доказательстве Isar. Вот фрагмент кода (он может зависеть от предыдущих частей доказательства, но это маловероятно). n относится к типу физ. ... then have 4:"2 ≤...

Я заинтересован в использовании Isabelle / Isar для написания доказательств, которые могут быть прочитаны человеком и проверены машиной, и я хочу улучшить свой стиль и упростить свои доказательства. prog-proof предлагает следующее упражнение:...