Rust 一阶逻辑

一阶逻辑语法的 Rust 实现，以及一个逻辑 'harness'，用于在论域上做出自洽的逻辑断言。

目标:

• 使用一阶逻辑的语法构造和操作逻辑语句。
• 定义和断言谓词和函数，并进行自洽的逻辑检查
• 提供一个接口，用于集成实现（独立于本包）高级数学概念（如集合论）的包，并通过 FOL 语言与之交互。

非目标:

• 实现任何集合论的形式，或展示集合的概念。
• 自动定理证明
• 提供一个基础，可以在其上实现高级数学包。

特性

包结构

语法

定义了一阶逻辑的强类型语法，包括一系列强类型范式和它们之间的转换方法。

语义

定义了一个内存中的图结构，用于跟踪逻辑语句并允许进行自洽的逻辑检查。

该图很少直接操作，而是由许多默认谓词和函数创建的公共接口管理。