pocket_prover 0.18.0

A fast, brute force, automatic theorem prover for first order logic
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35

use pocket_prover::*;

fn main() {
    println!("PSL: {}", prove!(&mut |
        (a, b), (t, u)
    | {
        imply(
            and!(
                imply(a, t),
                imply(b, u),
                not(eq(t, u)),
            ),
            and!(
                not(eq(a, b))
            )
        )
    }));

    println!("PSQ: {}", measure(100, || prove!(&mut |
        a, b, t, u
    | {
        imply(
            and!(
                imply(a, t),
                imply(b, u),
                not(eq(t, u)),
                imply(eq(a, b), q(a, b)),
                ps_core(a, b, t, u),
            ),
            and!(
                not(eq(a, b))
            )
        )
    })));
}