最后一阶逻辑

一种实验性的逻辑语言。

基于论文最后一阶逻辑。

=== Last Order Logic 0.2 ===
Type `help` for more information.
> a := 1 ~= 0
a := 1 ~= 0
LOL: Added `a` to definitions
> a ~ 0
a ~ 0
> ty
1

要从您的终端运行LOL，请输入

cargo install --example lolz last_order_logic

然后，要运行

lolz

如何学习LOL

要学习如何使用LOL，请在LOLZ中输入"help"。此命令列出所有主题，例如"help path"。

示例

• 几何综合

动机

在一阶逻辑中，量词表达式的真值取决于评估。这意味着自动定理证明器必须对表达式进行标注以真值，以便在修改源代码时高效地运行。语言的使用者无法直接访问这些信息。

最后一阶逻辑弥合了可用性和自动定理证明之间的差距。

• 提高可读性和改进通信
• 有效重用真值
• 可扩展到高阶真值

例如

∀ x { ... } - 很难看出这是 true 还是 false。

换句话说，一阶逻辑在计算上不是进步的。

最后一阶逻辑通过让量词表达式评估为自身，而真值编码在类型中，来解决此问题。

∀ x : I { ... } : un(1) - 很容易看出这是 true。

类型用于传达程序的意图。最后一阶逻辑使用此功能来提高可读性。

un(..) 语法表示“统一”，其中 un(1) 表示 ∀，而 un(0) 表示 ∃。相应地，nu(..) 表示“非统一”，其中 nu(1) 表示 ∃，而 nu(0) 表示 ∀。

另一个原因是表达路径上的真值，例如 un(0 ~= 1)。这些都是高维真值，不能用一阶逻辑表达。

统一与非统一真值的区别源于Avatar Extensions理论。只有非统一真值才有有意义的示例来显示其真值。

文件格式

• 常规文本格式 (.lol.txt)
• Markdown文本格式 (.lol.md)

Markdown格式是为了提高可读性设计的

• 必须以 # (Markdown标题) 开头
• 代码块必须使用 3 个反引号和 lol

LOLZ环境中的特殊命令不受支持。要引用LOLZ的使用，请使用 3 个反引号和 text。