Caso

交换图范畴理论求解器。

=== Caso 0.2 ===
Type `help` for more information.
> (A <-> B)[(A <-> C) -> (B <-> D)] <=> (C -> D)
(A <-> B)[(A <-> C) -> (B <-> D)] <=> (C <-> D)

要在您的终端中运行 Case，请输入

cargoinstall --examplecaso caso

然后，要运行

caso

语法

Caso 中的交换图使用以下语法编写

<左侧>[<顶部> -> <底部>] <=> <右侧>

此语法基于 路径语义 的表示法。

Caso 自动纠正方向错误，例如，当您输入 (a -> b)[(c -> a) -> ...] <=> ...。中的 c 相对于 a 是错误的，因此 Caso 将其更正为 (a -> b)[(a <- c) -> ...] <=> ...。

通过在箭头中计数 -（1）和 =（2）支持高阶同态。例如，<-> 是 1-同构，而 <=> 是 2-同构。

如何求解三角形

可以使用恒等同态将三角形展开为交换方形。

例如

> (A <-> B)[(A -> C) -> (B -> C)] <=> (C -> C)
(A <-> B)[(A -> C) -> (B -> C)] <=> (C <-> C)

在这里，C -> C 是从 C 到自身的恒等态射。

设计

Caso 使用 Avalog 作为单调求解器。

Avalog 规则位于 "assets/cat.txt"。

自动化定理证明器使用以下步骤

1. 解析表达式
2. 构造交换方阵
3. 使用范畴论规则扩展关于态射的知识
4. 分析新知识并将其重新整合到交换方阵中
5. 综合表达式。