程序员经验分享-hwhale

仅数学证明助理

2023-12-31

大多数证明助手都是具有依赖类型的函数式编程语言。他们可以证明程序/算法。相反，我感兴趣的是最适合数学且仅适合数学（例如微积分）的证明助手。你能推荐一个吗？我听说过 Mizar，但我不喜欢源代码被关闭，但如果它最适合数学，我会使用它。 Agda 和 Idris 等新语言有多适合数学证明？


Coq https://coq.inria.fr拥有涵盖实际分析的广泛库。我想到了各种发展：

  • the 标准库 https://coq.inria.fr/stdlib/以及以此为基础的项目，例如现已不复存在的项目coqtail https://github.com/coqtail/coqtail项目 [1]（广泛涵盖幂级数，并在复数方面做了大量工作）或更新的项目虞美人 http://coquelicot.saclay.inria.fr/。所有这些都依赖于实数的公理定义在此介绍 https://coq.inria.fr/stdlib/Coq.Reals.Raxioms.html.

  • 提出了更具建设性的方法C-CoRN http://corn.cs.ru.nl/项目从实际构建实数开始。

处理实数的另一种方法是转向非标准分析。这就是人们使用的ACL2 http://www.cs.utexas.edu/users/moore/acl2/一直在做。

为了更全面地了解该领域，您可能应该阅读这份调查报告 https://hal.inria.fr/hal-00806920v2由参与虞美人项目的人们设计。

[1] 全面披露：我参与了那个项目

本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)

proof

agda

idris

proofofcorrectness

isar

仅数学证明助理 的相关文章

  • 有限的数字如何运作？ （依赖类型）

    我对依赖类型语言感兴趣 有限数对我来说似乎非常有用 例如 安全地索引固定大小的数组 但这个定义对我来说并不清楚 Idris 中有限数的数据类型可以如下 Agda 中可能类似 data FiniteNum Natural gt Type wh

  • 当目标是类型时，为什么 Coq 不允许反转、析构等？

    When refine正在运行一个程序 我试图通过以下方式结束证明inversion on a False假设当目标是Type 这是我尝试做的证明的简化版本 Lemma strange1 forall T Type 0 gt 0 gt T

  • unionWith 的终止检查

    我在终止检查时遇到问题 与中描述的问题非常相似这个问题还有这个Agda 错误报告 功能请求 问题是让编译器相信以下内容unionWith终止 使用重复键的组合功能 unionWith合并表示为按键排序的 键 值 对列表的两个映射 有限映射的

  • 如何在 Idris 中表达范围有效性？

    我正在尝试在 Idris 中构建一个简单的调查表单 目前正在努力验证用户输入 该输入以字符串形式出现 所提出问题的类型 目前我有以下几种类型 data Question Type where QCM numOptions Nat gt qu

  • Haskell 中 Idris 的 Fin 的首选替代方案是什么

    我想要一个可以包含 0 到 n 值的类型 其中 n 位于类型级别 我正在尝试类似的事情 import GHC TypeLits import Data Proxy newtype FiniteNat n FiniteNat toIntege

  • 那么：有什么意义呢？

    其预期目的是什么So https github com idris lang Idris dev blob master libs base Data So idr L14类型 音译为阿格达 data So Bool Set where o

  • Agda 函数、类型匹配函数

    我想创建一个辅助函数 它将从索引或参数化类型中获取术语并返回该类型参数 showLen len A Set gt Vec A len gt showLen len showType len A Set gt Vec A len gt Set

  • 显示 (head .unit ) = Agda 中的 head

    我试图证明 Agda 中的一个简单引理 我认为这是正确的 如果向量有两个以上元素 则取其head继采取init与取其相同head立即地 我将其表述如下 lem headInit l xs Vec suc suc l gt head init

  • 仅数学证明助理

    大多数证明助手都是具有依赖类型的函数式编程语言 他们可以证明程序 算法 相反 我感兴趣的是最适合数学且仅适合数学 例如微积分 的证明助手 你能推荐一个吗 我听说过 Mizar 但我不喜欢源代码被关闭 但如果它最适合数学 我会使用它 Agda

  • 在 Agda 中对 ST monad 进行建模

    最近这个所以问题 https stackoverflow com questions 33975270 can a st like monad be executed purely without the st library促使我在 Ha

  • 理解 `k : Nat ** 5 * k = n` 签名

    以下函数编译 onlyModByFive n Nat gt k Nat 5 k n gt Nat onlyModByFive n k 100 但有什么作用k以其代表Nat 5 k n syntax 另外 我该如何称呼它 这是我尝试过的 但我

  • 如何解释agda中的REL

    我试图理解 Agda 标准库的某些部分 但我似乎无法弄清楚REL FWIW 这是定义REL Binary relations Heterogeneous binary relations REL a b Set a Set b Level

  • 如何处理 Agda 不确定是否在 with 语句中生成构造函数的情况？

    我有以下代码 open import Data Nat open import Agda Builtin Char open import Data Maybe digit Maybe digit n with compare n prim

  • 阿格达。冒号之前/之后的参数

    定义数据类型时 我可以在冒号之前 传递 一些参数 data Image A B Set f A B B Set where im f A B x A Image f f x 但出于未知原因 我似乎无法在函数声明中执行此操作 exIm A B

  • 使用 SPARK 证明选择排序算法

    我试图证明我在 Ada 中的选择排序实现是正确的 我尝试了一些循环不变量 但使用 gnatprove 只能证明内部循环的不变量 package body Selection with SPARK Mode is procedure Sort

  • 如何学习阿格达

    我正在努力学习agda 但是 我遇到了一个问题 我在 agda wiki 上找到的所有教程对我来说都太复杂了 并且涵盖了编程的不同方面 在并行阅读了 3 个关于 agda 的教程后 我能够编写简单的证明 但我仍然没有足够的知识来使用它来实现

  • 稳定的比较排序，时间复杂度为 O(n * log(n))，空间复杂度为 O(1)

    在经历的同时维基百科的排序算法列表 https secure wikimedia org wikipedia en wiki Sorting algorithm Comparison of algorithms我注意到没有稳定的比较排序 h

  • Coq 中的案例分析证明

    我试图证明关于以下函数的命题 Program Fixpoint division m nat n nat measure m nat match lt nat 0 n with false gt 0 true gt match leq na

  • 约束接口中的函数参数

    在接受函数的接口中约束函数参数的语法是什么 我试过 interface Num a gt Color f a gt Type where defs 但它说Name a is not bound in interface Your inter

  • Idris - 在 n 维向量上映射操作

    我在 Idris 中定义 n 维向量如下 import Data Vect NDVect Num t gt rank Nat gt shape Vect rank Nat gt t Type gt Type NDVect Z t t NDV

随机推荐

  • 有没有办法避免 Python list.append() 随着列表的增长而在循环中逐渐变慢？

    我正在读取一个大文件 并将每隔几行转换为对象的实例 由于我正在循环访问文件 因此我使用 list append instance 将实例存储到列表中 然后继续循环 该文件大小约为 100MB 因此并不算太大 但随着列表变大 循环速度会逐渐减

  • ActionBar 菜单项选择器 [关闭]

    Closed 这个问题需要细节或清晰度 help closed questions 目前不接受答案 是否可以在按下时更改菜单项的图像 并且可以通过选择器来完成 按下或选择时不同的菜单项应使用不同的图像进行更改 一些示例代码会很好 我查了很多

  • 使用 Python 通过 Google API 将电子表格复制到另一张电子表格

    我正在尝试从模板创建一个谷歌电子表格 然后编辑其值 单元格 我只需手动访问原始电子表格并单击复印一份来自File菜单 我还没有找到使用 Python3 和 gspread 来做到这一点的方法 因此 我正在尝试寻找解决方法 因此 我使用 Py

  • withNavigation 只能用于导航器的视图层次结构

    我收到错误 不变违规 withNavigation 只能在视图上使用 导航器的层次结构 被包装的组件无法获取 从 props 或 context 访问导航 我不知道为什么 因为我正在使用withNavigation在我的应用程序的其他组件中

  • 将所有互联网流量从我的 Android VoIP 应用程序路由到我自己的 VPN 服务器

    我们已经设置了您自己的 VPN 服务器 并希望通过此服务器路由来自您的 VOIP android 应用程序的所有流量 但到目前为止我看到的所有解决方案都使用 vpn 服务类http developer android com referen

  • 友好 URL（mod 重写）问题

    Hallo 我正在尝试创建 漂亮 的 URL 第一条规则按预期工作 它正在转动 www blabla com index php page tags tag blabla into www blabla com tags blabla 但第

  • Flutter - 更改堆栈顺序

    我有一个堆栈 在某种条件下 例如用户单击 我希望将较低顺序的小部件之一推到堆栈的顶部 使用下面的代码作为一个简单的示例 在 setState 方法中我需要什么代码来重新排序 以便第一个 底部 小部件成为最后一个 顶部 小部件 new Sta

  • 非静态字段、方法或属性需要对象引用

    我想以所有形式传递 myConnString 我正在 winform 和 mysql C 中工作 所以我尝试了这个链接 http www daniweb com software development csharp threads 499

  • 模板类限制[重复]

    这个问题在这里已经有答案了 我想知道是否有任何方法可以限制使用自定义条件为模板生成代码 在我的情况下 我想仅当模板类 T 已由类 bar 继承时才调用 foo 函数 类似这样 template

  • 为什么其他程序看不到我在 VS Code 中对文件所做的更改，直到我保存这些更改？

    我注意到当我在 VS Code 中更改文件时 另请参阅VS Code 选项卡手柄上有一个白点意味着什么 https stackoverflow com q 76024956 11107541 在我保存这些更改之前 其他程序仍会看到该文件的上

  • 正则表达式 - URL 中的希腊字符

    我有一个使用正则表达式的自定义路由器 问题是我无法解析希腊字符 以下是一些来自index php router gt get theatre plays TheatreController showPlays router gt get t

  • 分解旋转矩阵 (x,y',z'') - 笛卡尔角度

    分解旋转矩阵 x y z 笛卡尔角度 我目前正在与旋转矩阵我有以下问题 给定三个坐标系 O0 x0 y0 z0 O1 x1 y1 z1 O2 x2 y2 z2 这一致 我们首先相对于帧 0 旋转帧 1 然后相对于帧 1 旋转帧 2 旋转的顺

  • 导入错误：无法导入名称“getLogger”

    这个问题在这里已经有答案了 但似乎我遇到了一种无法用答案解释的情况 详细信息如下 我有一个名为logging py 的文件 代码如下 import sys print sys path from logging import getLogg

  • “应用程序包的顶层”在哪里？在 XCode 中

    我试图将 Default png 图像放入我的 iPhone 应用程序中 但无法弄清楚 应用程序包的顶层 在 XCode 窗口中的位置 在压缩发布之前 您是否不将其添加到 Xcode 中 而是添加到构建文件中 只需将其添加到您的项目中即可

  • 在 Unity 中注册类型时如何传入构造函数参数？

    我在 Unity 中注册了以下类型 container RegisterType

  • 使用 mod_wsgi 记录烧瓶错误

    很长一段时间以来我一直在努力让它发挥作用 但现在我真的束手无策 我已经尝试做我可以在 SO 和 Flask 文档中找到的所有内容 但仍然无法使用简单的错误日志来调试我的应用程序 下面是粘贴的代码 main py from flask imp

  • Powershell - “表达式只允许作为管道的第一个元素”

    在以下情况下如何避免此错误 codegenDir Z Desktop Song Renamer PowerShellRepresentation dir path MyMusicFolder recurse include mp3 m4a

  • CSS 停止图像下的文本换行

    我有以下标记 li img class fav star src images fav png span Text text and more text span li 我希望这样 如果文本换行 它就不会进入图像的 列 我知道我可以用tab

  • 清除网络浏览器控件中的选择

    我有一个带有网络浏览器控件的表单 我将所有文本 不是 html 数据复制到剪贴板 为此 代码片段是 webBrowser2 Document ExecCommand SelectAll false null webBrowser2 Docu

  • 仅数学证明助理

    大多数证明助手都是具有依赖类型的函数式编程语言 他们可以证明程序 算法 相反 我感兴趣的是最适合数学且仅适合数学 例如微积分 的证明助手 你能推荐一个吗 我听说过 Mizar 但我不喜欢源代码被关闭 但如果它最适合数学 我会使用它 Agda

热门标签