raa_tt 0.1.0

Proves sentences of propositional calculus
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

// To run the test please issue:
// cargo run ./test.txt

// Not L-True
// (p -> (!p & r))

// !p -> q

// L-True
// p | q | !p

// a -> b -> c -> d

// L-True
// ((p & q) -> p)


// Contingent
// ((p | q) -> (r -> p))

// L-True
// p -> (q -> r | p)

// L-True
// p & q -> p

// L-True
// (p -> q) -> ((q -> r) -> (p -> r))

// Contingent
// !((!p | !q) & (p <-> !r) -> !(q & r))

// Contingent
// p & q <-> !(p & q) | !q

// p & !p

// p | !p

// (!p | !q) & (p <-> !r) -> !(q & r)

// Contingent
// !(p & q <-> !(p & q) | !q)

// L-True - Modus Ponens
// p & (p -> q) -> q

// L-True - Disjunctive syllogism
// (p | q) & !p -> q

// Contingent
// q & (p -> q) -> p

// L-True
p -> q -> (p & r -> p)