Pocket-Prover

用于一阶逻辑的快速、穷举、自动定理证明器

• 有关通用自动定理证明，请参阅 monotonic_solver
• 有关可调试的SAT求解器，请参阅 debug_sat

extern crate pocket_prover;

use pocket_prover::*;

fn main() {
    println!("Socrates is mortal: {}", prove!(&mut |man, mortal, socrates| {
        // Using `imply` because we want to prove an inference rule.
        imply(
            // Premises.
            and(
                // All men are mortal.
                imply(man, mortal),
                // Socrates is a man.
                imply(socrates, man),
            ),

            // Conclusion.
            imply(socrates, mortal)
        )
    }));
}

动机

动机是提供一个类似于“口袋计算器”的逻辑版本，因此称为“口袋证明器”。

此库使用的方法是在低级语言中从头开始实现的方法。

这在以下情况下很有用

• 学习逻辑，无需克服手动证明的障碍
• 检查你对逻辑的理解
• 验证逻辑学家是巫师而不是爬行动物
• 由于一系列不幸的事件，你只有24小时学习逻辑，只需要了解其精髓
• 为了记住类似《火星救援》中的源代码
• 一个小错误就会让整个星球爆炸（例如，在AI奇点之前的最终决策，你需要按下正确的按钮）

此外，此库可用于创建可扩展的逻辑系统。更多信息，请参阅 Prove 特性。

实现

此库使用穷举法检查证明，而不是依赖于逻辑公理。

64位CPU能够以O(1)的速度检查6个参数（布尔值）的逻辑证明，因为证明可以解释为重言式（对所有输入都为真）并且 bool 可以替换为 u64，并使用位模式组织输入，模拟6个参数的真值表。

这是通过将 bool 替换为 u64 并使用位模式组织输入来实现的，这些位模式模拟了6个参数的真值表。

要扩展到10个参数，使用 T 和 F 来交替4个额外的参数。要扩展到N个参数，使用递归调用，直到少于10个参数。

路径语义逻辑

注意！路径语义逻辑处于研究初期阶段。

该库对路径语义逻辑的一个子集提供实验性支持。实现基于论文快速暴力证明。

路径语义逻辑将命题分为不同级别，使得在N+1级别上两个命题之间的等价性可以传播到N级别上唯一关联的命题之间。

例如，如果f的级别为1，而x的级别为0，那么imply(f, x)将x唯一关联到f上，使得路径语义的核心公理得到满足。

该库目前仅支持级别1和0。这些函数以path1_为前缀。

宏count!和prove!将自动展开为path1_count!和path1_prove!。

每个函数接受两个参数，由命题的元组组成，例如(f, g), (x, y)。支持任意数量的参数。

extern crate pocket_prover;

use pocket_prover::*;

fn main() {
    println!("=== Path Semantical Logic ===");
    println!("The notation `f(x)` means `x` is uniquely associated with `f`.");
    println!("For more information, see the section 'Path Semantical Logic' in documentation.");
    println!("");

    print!("(f(x), g(y), h(z), f=g ⊻ f=h) => (x=y ∨ x=z): ");
    println!("{}\n", prove!(&mut |(f, g, h), (x, y, z)| {
        imply(
            and!(
                imply(f, x),
                imply(g, y),
                imply(h, z),
                xor(eq(f, g), eq(f, h))
            ),
            or(eq(x, y), eq(x, z))
        )
    }));

    print!("(f(x), g(y), f=g => h, h(z)) => (x=y => z): ");
    println!("{}\n", prove!(&mut |(f, g, h), (x, y, z)| {
        imply(
            and!(
                imply(f, x),
                imply(g, y),
                imply(eq(f, g), h),
                imply(h, z)
            ),
            imply(eq(x, y), z)
        )
    }));
}

路径语义质量

Pocket-Prover具有类似于量子逻辑的路径语义质量模型。

要写入x ~~ y，您可以使用q(x, y)或qual(x, y)。

q(x, y)与and!(eq(x, y), qubit(x), qubit(y))相同。q(x, x)与qubit(x)相同。

量子比特是一种“叠加”。也可以将其视为引入一个依赖于x的新参数qubit(x)。

由于量子比特可以与其他命题发生碰撞，因此必须重复测量（例如使用measure）以获得经典状态。然而，有时可能希望放大量子状态，使用amplify或amp。

要使用路径语义与质量，应使用ps_core。路径语义逻辑是为等价性设计的，而不是为质量设计的。

use pocket_prover::*;

fn main() {
    println!("Path semantics: {}", measure(1, || prove!(&mut |a, b, c, d| {
        imply(
            and!(
                ps_core(a, b, c, d),
                imply(a, c),
                imply(b, d)
            ),
            imply(qual(a, b), qual(c, d))
        )
    })));
}