inference_rules/
inference_rules.rs

1extern crate pocket_prover;
2
3use pocket_prover::*;
4
5fn main() {
6    println!("Inference rules:");
7    // Truth value can be derived from any premise.
8    println!("  true-conclusion: {}", prove!(&mut |a| imply(
9        a,
10        T
11    )));
12    // Anything can be derived from a false premise.
13    println!("  false-premise: {}", prove!(&mut |a| imply(
14        F,
15        a
16    )));
17
18    println!("  modus-ponens: {}", prove!(&mut |p, q| imply(
19        and(
20            imply(p, q),
21            p,
22        ),
23        q
24    )));
25    println!("  modus-tollens: {}", prove!(&mut |p, q| imply(
26        and(
27            imply(p, q),
28            not(q)
29        ),
30        not(p)
31    )));
32    println!("  hypothetical-syllogism: {}", prove!(&mut |p, q, r| imply(
33        and(
34            imply(p, q),
35            imply(q, r),
36        ),
37        imply(p, r)
38    )));
39    println!("  disjunctive-syllogism: {}", prove!(&mut |p, q| imply(
40        and(
41            or(p, q),
42            not(p),
43        ),
44        q
45    )));
46    println!("  addition: {}", prove!(&mut |p, q| imply(
47        p,
48        or(p, q)
49    )));
50    println!("  simplification: {}", prove!(&mut |p, q| imply(
51        and(p, q),
52        p
53    )));
54    println!("  conjunction: {}", prove!(&mut |p, q| imply(
55        and(
56            p,
57            q,
58        ),
59        and(p, q)
60    )));
61    println!("  resolution: {}", prove!(&mut |p, q, r| imply(
62        and(
63            or(not(p), r),
64            or(p, q),
65        ),
66        or(q, r)
67    )));
68}
inference_rules/inference_rules.rs

inference_rules/
inference_rules.rs
