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
71
72
73
74
75
76
77
78
79
80

#![allow(non_snake_case)]

use pocket_prover::*;

fn main() {
    println!("Water: {}", measure(100, || prove!(&mut |H, O, a, b, c| {
        imply(
            water(H, O, a, b, c),
            eq(q(a, b), q(b, c))
        )
    })));

    println!("Salt: {}", measure(100, || prove!(&mut |Na, Cl, a, b| {
        imply(
            salt(Na, Cl, a, b),
            atom(b, Cl)
        )
    })));

    println!("Oxygen: {}", measure(100, || prove!(&mut |O, Bond2, a, b| {
        imply(
            oxygen(O, Bond2, a, b),
            bond(a, b, Bond2)
        )
    })));
}

pub fn atom(a: u64, atom: u64) -> u64 {eq(q(a, a), atom)}
pub fn bond(a: u64, b: u64, bond: u64) -> u64 {and(eq(a, b), eq(q(a, b), bond))}
pub fn react2(a: [u64; 2], b: [u64; 2]) -> u64 {
    and!(
        xor!(
            and(
                eq(a[0], b[0]),
                eq(a[1], b[1])
            )
        )
    )
}

pub fn water(H: u64, O: u64, a: u64, b: u64, c: u64) -> u64 {
    and!(
        atom(a, H),
        atom(b, O),
        atom(c, H),
        eq(a, b),
        eq(b, c),
    )
}

pub fn salt(Na: u64, Cl: u64, a: u64, b: u64) -> u64 {
    and!(
        atom(a, Na),
        atom(b, Cl),
        eq(a, b)
    )
}

pub fn methane(H: u64, C: u64, a: u64, b: [u64; 4]) -> u64 {
    and!(
        atom(a, C),
        atom(b[0], H),
        atom(b[1], H),
        atom(b[2], H),
        atom(b[3], H),
        eq(a, b[0]),
        eq(a, b[1]),
        eq(a, b[2]),
        eq(a, b[3]),
    )
}

pub fn oxygen(O: u64, E2: u64, a: u64, b: u64) -> u64 {
    and!(
        atom(a, O),
        atom(b, O),
        bond(a, b, E2),
        eq(a, b),
    )
}