文件名称：logic:通用证明检查库
文件大小：24KB
文件格式：ZIP
更新时间：2024-05-03 01:48:49
Rust
校对员 用于检查正式构造的证明的库。 用法 该库的内容： 表示Formlae和演绎步骤的对象和类。 它还提供了全面检查数学证明所需的必要接口。 还有一些通常在形式逻辑中通常不考虑的额外结构。 包括一些非标准结构； 具体来说，一些值得注意的结构是 模式：通用二阶逻辑（ZFC要求） 顺序变量：对定义内联集表示法很有用 ForAllSeq（对于所有有限的非空序列）：对定义内联集表示法很有用。 Lambda：在定义理论中的功能时很有用。 该库没有什么： 该库不是自动证明系统：证明必须通过人工或其他系统构建，并且由客户维护检查证明所需的知识基础。 例子： 模块中存在许多示例，这些示例演示了一些证明的“软件内”实现。 一些例子： 平等： 请参阅以获取有关相等性的某些标准属性的证明。 德摩根定律： 参见，其中为DeMorgan定律的一部分构建了软件定理和证明。
【文件预览】：
logic-master
----src()
--------theorems()
--------writing.rs(25KB)
--------expr.rs(23KB)
--------formed.rs(4KB)
--------deduction.rs(26KB)
--------subst.rs(7KB)
--------lib.rs(201B)
--------knowledge_base.rs(9KB)
--------formula.rs(26KB)
----Cargo.toml(105B)
----.gitignore(320B)
----README.md(1KB)