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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55

use pocket_prover::*;

fn main() {
    let n = 100;

    // true
    println!("Sesh: {}", measure(n, || prove!(&mut |a| {
        eq(not(qu(a)), qu(not(a)))
    })));

    // false
    println!("Platonic Sesh: {}", measure(n, || prove!(&mut |a| {
        eq(not(pqu(a)), pqu(not(a)))
    })));

    // false
    println!("Platonic Eq Not: {}", measure(n, || prove!(&mut |a| {
        eq(pqu(a), pqu(not(a)))
    })));

    // true
    println!("Composite Sesh: {}", measure(n, || prove!(&mut |a| {
        eq(not(re_sesh(pqu(a))), re_sesh(pqu(not(a))))
    })));

    // true
    println!("Eq: {}", measure(n, || prove!(&mut |a| {
        eq(re_sesh(pqu(a)), qu(a))
    })));

    // true
    println!("Sesh Id: {}", measure(n, || prove!(&mut |a| {
        eq(re_sesh(un_sesh(a)), a)
    })));

    // true
    println!("Sesh Inv Id: {}", measure(n, || prove!(&mut |a| {
        eq(un_sesh(re_sesh(a)), a)
    })));

    // false
    println!("Sesh Un-Qu-Re: {}", measure(n, || prove!(&mut |a| {
        eq(re_sesh(qubit(un_sesh(a))), qubit(a))
    })));

    // false
    println!("Sesh Re: {}", measure(n, || prove!(&mut |a| {
        eq(re_sesh(a), a)
    })));

    // false
    println!("Sesh Re == Un: {}", measure(n, || prove!(&mut |a| {
        eq(re_sesh(a), un_sesh(a))
    })));
}