一个定理证明器/证明助手支持（多个）子类型化/子类化

Question

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

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

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。

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

在选择您的系统时，特定低级功能的列表并不是那么相关。在做出承诺之前，您喜欢系统的总体风格和文化更为重要。你可以把它比作学习一门外语。在你花几个月或几年的时间学习之前，你是否收集了语法的特征？我不这么认为。