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

extern crate pocket_prover;

use pocket_prover::*;

fn main() {
    println!("Inference rules:");
    // Truth value can be derived from any premise.
    println!("  true-conclusion: {}", prove!(&mut |a| imply(
        a,
        T
    )));
    // Anything can be derived from a false premise.
    println!("  false-premise: {}", prove!(&mut |a| imply(
        F,
        a
    )));

    println!("  modus-ponens: {}", prove!(&mut |p, q| imply(
        and(
            imply(p, q),
            p,
        ),
        q
    )));
    println!("  modus-tollens: {}", prove!(&mut |p, q| imply(
        and(
            imply(p, q),
            not(q)
        ),
        not(p)
    )));
    println!("  hypothetical-syllogism: {}", prove!(&mut |p, q, r| imply(
        and(
            imply(p, q),
            imply(q, r),
        ),
        imply(p, r)
    )));
    println!("  disjunctive-syllogism: {}", prove!(&mut |p, q| imply(
        and(
            or(p, q),
            not(p),
        ),
        q
    )));
    println!("  addition: {}", prove!(&mut |p, q| imply(
        p,
        or(p, q)
    )));
    println!("  simplification: {}", prove!(&mut |p, q| imply(
        and(p, q),
        p
    )));
    println!("  conjunction: {}", prove!(&mut |p, q| imply(
        and(
            p,
            q,
        ),
        and(p, q)
    )));
    println!("  resolution: {}", prove!(&mut |p, q, r| imply(
        and(
            or(not(p), r),
            or(p, q),
        ),
        or(q, r)
    )));
}