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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70

/*

This example shows that the Creation Theorem is not a tautology
in the model of path semantical quality that resembles quantum logic.

This means that this model of quality gives rise to a new logic:

   Path Semantical Quantum Propositional Logic (PSQ)

*/

use pocket_prover::*;

fn main() {
    println!("Creation Theorem: {}", measure(10, || prove!(&mut |a, b, a2, b2| {
        creation(a, b, a2, b2)
    })));

    println!("");
    for i in 1..10 {
        for _ in 0..50 {
            if measure(i, || prove!(&mut |a, b, c, d| creation(a, b, c, d))) {
                print!("1");
            } else {
                print!("0");
            }
        }
        println!("");
    }
    println!("");

    println!("Creation Theorem with EqQ: {}", measure(10, || prove!(&mut |a, b, a2, b2| {
        creation_with_eqq(a, b, a2, b2)
    })));

    println!("");
    for i in 1..10 {
        for _ in 0..50 {
            if measure(i, || prove!(&mut |a, b, c, d| creation_with_eqq(a, b, c, d))) {
                print!("1");
            } else {
                print!("0");
            }
        }
        println!("");
    }
}

pub fn creation(a: u64, b: u64, a2: u64, b2: u64) -> u64 {
    imply(
        and!(
            ps_core(a, b, a2, b2),
            not(a),
            imply(b, b2),
        ),
        imply(a2, b2)
    )
}

pub fn creation_with_eqq(a: u64, b: u64, a2: u64, b2: u64) -> u64 {
    imply(
        and!(
            imply(eq(a, b), q(a, b)),
            ps_core(a, b, a2, b2),
            not(a),
            imply(b, b2),
        ),
        imply(a2, b2)
    )
}