haskell - 支持(多个)子类型化/子类化的定理证明者/证明助手

Question

已结束。此问题正在寻求书籍、工具、软件库等的推荐。它不满足 Stack Overflow guidelines 。目前不接受答案。

---

我们不允许提出寻求书籍、工具、软件库等推荐的问题。您可以编辑问题，以便用事实和引文来回答。

已关闭 8 年前。

Improve this question

简而言之，我正在寻找一个定理证明器，其底层逻辑支持多种子类型/子类化机制。(我尝试使用 Isabelle，但它似乎没有为子类型提供一流的支持。see this )

我想定义几种类型，其中一些是其他类型的子类/子类型。此外，每种类型可能是多个类型的子类型。例如:

Type A
Type B
Type C
Type E
Type F

C is subtype of A
C is also subtype of B
E and F are subtypes of B

PS:我再次编辑这个问题以使其更加具体(因为提示偏离主题!):我正在寻找一个定理证明者/证明帮助，我可以在其中以直接的方式定义上述结构(而不​​是使用解决方法)正如这里一些值得尊敬的答案所友好描述的那样)。如果我将类型视为类，那么上面的子类型似乎可以 轻松用 C++ 来表述!所以我正在寻找一个正式的系统/工具，我可以在那里定义这样的子类型结构，并且我可以推理？

非常感谢

Answer 1

PVS传统上非常强调“谓词子类型”，但现在该系统有点过时，并且已经落后于其他更活跃的大玩家:Coq、Isabelle/HOL、Agda、其他 HOL、ACL2。

您没有明确说明您的申请。我认为任何大型系统都可以以某种方式应用于该问题。形式化是指在给定的逻辑环境中以适当的方式表达问题。逻辑不是编程语言，但具有数学的真正力量。因此，凭借在特定逻辑方面的一些经验，您将能够做出您乍一看没有想到的伟大而令人惊奇的事情。

在选择系统时，特定低级功能的列表并不那么相关。在做出 promise 之前，更重要的是您喜欢系统的总体风格和文化。您可以将其与学习外语进行比较。在花费数月或数年的时间学习之前，您是否收集了语法特征？我不这么认为。