|
1
EC, ID, DN, IC
|
-1 (s -> t) & (r & t)
I- (s -> t) & r
|
|
2
EC, ID, DN, IC
|
-1 (p & q) & (r & s)
I- p & r
|
|
3
EC, ID, DN, IC
|
-1 (p
-> q) & ¬¬ (r v q)
I- (p -> q) & ( r
v s)
|
|
4
EC, ID, DN, IC
|
-1 p & (q & r)
I- (p & q) & r
|
|
5
MP
|
-1. t
-> q
-2. s v r -> v
-3. v & q -> p
-4. t & s
I- p
|
|
6
IB
|
-1. p v q -> (q -> p & q)
-2. r & (p & q -> q)
-3. ¬¬p
I- q <-> p & q->
|
|
7
IB
|
-1. p & ¬¬(q -> r)
-2. r -> q
I- q <-> r->
|
|
8
EB
|
-1. p
<-> q->
-2. r <-> (p &
q)->
-3. ¬¬p
I- r v s
|
|
9
EB
|
-1. p
<-> t->
-2. ¬s <-> t->
-3. ¬¬ (t -> ¬s)
<-> ¬¬q->
-4. p
I- p & q
|
|
10
IN
|
-1 p & q -> r
-2 r -> s
-3 q & ¬s
I- ¬p
|
|
11
IN
|
-1 q & (r <-> q)->
-2 ¬ r -> p
I- ¬ r
|
|
12
IC
|
-1 t
-> q
-2 w -> r
-3 r & q -> p
I- t & w -> p
|
|
13
IC
|
-1 p -> r
-2 ¬ (q -> r)
I- ¬ (q -> p)
|
|
14
IC
|
-1 p -> (q -> r)
-2 s -> p & q
I- ¬¬s -> r
|
|
15
IC
|
-1 p & q -> r
I- p -> (q -> r)
|
|
16
ED
(144)
|
- 1 ¬q
-> r
- 2 t -> ¬ q
- 3 ¬ s -> ¬ q
I-t v ¬s -> r
|
|
17
ED
|
-1 p
-> q
-2 r -> p
-3 t -> r
-4 s -> r
-5 t v s
I- q v ¬w
|
|
18
ED
|
-1 p
& (q v r)
I- (p & q) v (p &
r)
|
|
19
ED
|
-1 (p v
q) v r
I- p v (q v r)
|
|
20
REGLAS BÁSICAS
|
-1 q -> ¬p
-2 r -> q
-3 r
I- ¬p
|
|
21
REGLAS BÁSICAS
|
-1 ¬ p -> ¬ q
-2 s v ¬q -> ¬¬ r
-3 ¬p
I- r
|
|
22
REGLAS BÁSICAS
|
-1 p <-> ¬¬ (q & r)->
-2 q & (r -> s)
-3 p
I- s
|
|
23
REGLAS BÁSICAS
|
-1 ¬p
<-> q->
-2 s v t -> ¬p
-3 ¬¬ s
I- q v r
|
|
24
REGLAS BÁSICAS
|
-1 p
-2 p -> ¬ q
-3 p & ¬q -> ¬¬s
-4 s -> ¬¬ t
I- t
|
|
25
REGLAS BÁSICAS
|
-1 p
-2 p -> q
-3 ¬¬( q -> ¬ s)
I- ¬s
|
|
26
REGLAS DERIVADAS
|
-1 p -> q
I- ¬q -> ¬p
|
|
27
REGLAS DERIVADAS
|
-1 ¬ p -> ¬q
-2 q
I- p
|
|
28
REGLAS DERIVADAS
|
-1 q & r -> ¬s
-2 s
I- ¬q v ¬r
|
|
29
REGLAS DERIVADAS
|
-1 p -> q & r
-2 ¬ q v ¬ r
I- ¬p
|
|
30
REGLAS DERIVADAS
|
-1 p v q -> r
-2 ¬ r
I- ¬q
|
|
31
REGLAS DERIVADAS
|
-1 ¬ p
-2 q -> p
-3 ¬q -> r
I- r v s
|
|
32
REGLAS DERIVADAS
|
-1 p v q
-2 q -> t
-3 ¬ t
I- p
|
|
33
REGLAS DERIVADAS
|
-1 ¬r v
¬q
-2 t v s -> r
-3 q v ¬s
-4 ¬t
I- ¬(t v s)
|
|
34
REGLAS DERIVADAS
|
-1 p v q
-2 t -> ¬p
-3 ¬(q v r)
I- ¬t
|
|
35
REGLAS DERIVADAS
|
-1 p
-> ¬s
-2 s v ¬r
-3 ¬ (t v ¬r)
I- ¬p
|
|
36
REGLAS DERIVADAS
|
-1 p
-> q v r
-2 q -> ¬p
-3 s -> ¬r
I- p -> ¬s
|
|
37
IC
|
-1 p v ¬s
-2 ¬r -> s
I- ¬p -> r
|
|
38
IC
|
-1 ¬(r & s)
-2 q -> s
I- r -> ¬q
|
|
39
IC
|
-1 s
-> r
-2 s v p
-3 p -> q
-4 r -> t
I- ¬q -> t
|
|
40
IC
|
-1 ¬s <-> t & p->
-2 r -> ¬ s
I- r-> t
|
|
41
IC
|
-1 s
& (¬p v t)
-2 t -> q v r
I- p -> (¬q -> r)
|
|
42
IC
|
-1 p
-> q
-2 q -> r
-3 r -> s v t
I- ¬s & ¬t -> ¬p
|
|
43
IC
|
-1 p v q
-> (r v s -> t)
I- p -> (r -> t)
|
|
44
IC
|
-1 ¬ q
-> ¬p
-2 p -> (q -> r)
-3 ¬(r -> s) -> ¬q
I- p -> s
|
|
45
IC
(146)
|
1
¬s v ¬p
-2 q -> ¬r
-3 t -> s &
r
I- t -> ¬(p v q)
|
|
46
IC
(136)
|
- 1 (r v
q) -> p
- 2 t -> (¬p&¬m)
- 3 t v s
I- r -> s
|
|
47
IN
|
-1 ¬ (p & q)
-2 ¬r -> ¬p
-3 ¬q -> ¬r
I- ¬p
|
|
48
IN
|
-1 t -> ¬s
-2 r -> ¬t
-3 s v r
I- ¬t
|
|
49
IN
|
-1 ¬(p & q)
-2 ¬ q -> r
-3 ¬r -> p
I- r
|
|
50
IN
|
-1 ¬(q v
r)
-2 t <-> ¬p->
-3 p v q
I- ¬t
|
|
51
IN
|
-1 s
-> ¬p
-2 s v ¬r
-3 ¬(t v¬r)
I- ¬p
|
|
52
IN
|
-1 p
-> q v r
-2 q -> ¬p
-3 s -> ¬r
I- ¬ (p & s)
|
|
53
IN
|
-1 ¬r -> ¬s
-2 t & r <-> ¬s->
I- r
|
|
54
IN
|
-1 ¬r v
¬q
-2 t v s -> r
-3 q v ¬s
-4 ¬t
I- ¬(t v s)
|
|
55
IN
(152)
|
-1 (p v q) -> (r & s)
-2 ¬r
I- ¬ p
|
|
56
IN
|
-1 s
-> p
-2 r v ¬ p
-3 t -> ¬r
I- ¬s v ¬t
|
|
57
IN
|
-1 p -> ¬ q
-2 r -> q
I- ¬(p & q)
|
|
58
IN
|
-1 ( ¬q -> ¬p) & (¬p -> q)
I- q
|
|
59
IN
|
-1 ¬(¬p
& ¬r)
-2 ¬s -> ¬r
-3 p -> q
I- q v s
|
|
60
IN
|
-1 ¬p
-> s v r
-2 ¬p & r
-3 s -> q
I- q v r
|
|
61
REGLAS DERIVADAS
|
-1 p v
¬(¬q & ¬r)
-2 ¬p & ¬q
I- r v s
|
|
62
IC
|
-1 ¬p -> q
-2 q -> ¬r
I- r -> p
|
|
63
IN
|
-1 p -> q
-2 ¬(p & r) & (r v ¬q)
I- ¬p
|
|
|
|
|
64
|
- 1 s
-> r
- 2 s v p
- 3 p -> q
- 4 r -> t
I- ¬ q -> t
|
|
65
|
- 1 t -> ¬s
- 2 q -> ¬t
- 3 s v q
I- ¬t
|
|
66
|
- 1
(m&n)-> ¬t
- 2 t v¬s
- 3 ¬ (p v ¬s)
I- ¬(m & n)
|
|
67
|
- 1 ¬ q v s
- 2 ¬s
- 3 ¬(r & s) -> q
I- r
|
|
68
|
- 1 p v¬r
- 2 ¬r -> s
- 3 p -> t
- 4 ¬s
I- t
|
|
69
|
- 1 p-> ¬(s v ¬r)
- 2 q -> ¬(m v r)
- 3 ¬(¬u & ¬p)
- 4 ¬(¬u & ¬q)
I- u
|
|
70
|
- 1 p
-> q
- 2 (p->r) -> (svq)
- 3 (p & q) -> r
- 4 ¬s
I- q
|
|
71
|
- 1 p
-> ¬r
- 2 q -> ¬s
- 3 m -> (r & s)
- 4 n -> (r & s)
- 5 t -> ¬¬m
- 6 ¬t -> ¬¬n
I- ¬p v ¬q
|
|
72
|
- 1 (t & r) <-> s->
- 2 ¬r -> ¬s
I- r
|
|
73
|
- 1 (p v
q) -> r
- 2 w-> ¬(m&s)
- 3 ¬(tvn) ->m
- 4 q <-> t v n->
- 5 s
I- w -> r
|
|
74
|
-
1(p->q) & (r -> s)
- 2 ¬q v ¬s
- 3 ¬(p & r)->t
I- t
|
|
75
|
- 1 ¬(¬q
v ¬t)
- 2 p -> m
- 3 n -> ¬q
- 4 p v n
I- m
|
|
76
|
- 1¬p ->
q
- 2 ¬m -> n
- 3 ¬r -> s
- 4 ¬s -> x
- 5 ¬(¬¬p v ¬¬m)
- 6¬(¬¬r v ¬¬s)
- 7 ¬(s -> ¬q) -> w
- 8 ¬(n -> ¬x)-> u
I- ¬(¬w v ¬u)
|
|
77
|
- 1
¬(pvq) ->r
- 2 ¬(w v m)
- 3 ¬(z v n)
- 4 ¬(mvn) ->t
- 5 ¬(svp)
- 6 ¬(u vq)
I-¬(¬r v¬t)
|
|
78
|
- 1 p -> w
- 2 q v ¬ w
- 3 ¬( p & q)
I- ¬ p
|
|
79
|
- 1 ¬(p & q)
- 2 ¬r -> q
- 3 ¬p -> r
I- r
|
|
80
|
- 1 p -> q
- 2 ¬ q
- 3 ¬ p -> ( r & s)
I- r & s
|
|
81
|
- 1 p
& q
- 2 r -> ¬q
- 3 ¬r -> s
I- s v¬p
|
|
82
|
- 1 r v s
- 2 ¬t -> ¬p
- 3 r -> ¬q
I- (p & q) -> (s
& t)
|
|
83
|
- 1 q
-> p
- 2 t v s
- 3 q v ¬s
I- ¬(p v r) -> t
|
|
84
|
- 1 p -> q
- 2 (p & q) -> r
- 3 ¬(p & r)
I- ¬p
|
|
85
|
- 1 r -> ¬p
- 2 ¬ (q & ¬r)
I- p -> ¬q
|
|
86
|
- 1(s
& ¬r) -> q
- 2(¬t & ¬q) -> w
- 3 t -> ¬m
- 4 s
- 5 ¬p v ¬q
- 6 ¬(¬m & r)
I- p -> w
|
|
87
|
- 1 ¬m v
p
- 2 q -> m
- 3 x v t
- 4 t -> (r & s)
- 5 ( s & r )->w
I-(¬p->¬q)->(¬w->x)
|
|
88
|
- 1
(p&q)->¬r
- 2 r v (s&t)
- 3 p <-> q->
I- p -> s
|
|
89
|
- 1
p->¬(¬rv¬s)
- 2 ¬¬s ->¬u
- 3 ¬m v n
- 4¬n
- 5 p & q
I-¬(u v m)
|
|
90
|
- 1 t -> m
- 2 ¬(u & p)
- 3 n ->¬m
- 4¬(¬p & ¬w)
- 5 ¬n -> ¬s
- 6 z -> u
- 7 ¬(r v ¬t)
- 8 ¬z -> s
I- w v q
|
|
91
|
- 1 ¬p
-> ¬ s
- 2 ¬p v r
- 3 r -> ¬t
I- ¬s v ¬t
|
|
92
|
- 1 ¬t v ¬r
- 2 ¬r -> p
- 3 ¬(¬r &p)
I- ¬t
|
|
93
|
- 1 r
-> s
- 2 s -> q
- 3 r v (s & t)
I- ¬q -> (t &s)
|
|
94
|
- 1 ¬r
-> s
- 2 s -> (p &q)
- 3 r -> t
- 4 ¬t
I- q
|
|
95
|
- 1 ¬s v ¬r
- 2 ¬r -> ¬t
- 3 ¬p
I- ¬t & ¬p
|
|
96
|
- 1 (r v
q) -> p
- 2 t -> (¬p&¬m)
- 3 t v s
I- r -> s
|
|
97
|
- 1 r
-> n
- 2 t -> (p v r)
- 3 (q v n) -> t
- 4 ¬n
I- ¬p -> ¬q
|
|
98
|
- 1 ¬q
-> ¬(mvt)
- 2 ¬r -> ¬(p&q)
- 3 ¬s -> p
- 4 ¬n-> t
I- ¬(r v s) -> n
|
|
99
|
- 1 p
-> q
- 2 p->(q -> r)
- 3 q->( r -> s)
I- p -> s
|
|
100
|
- 1 ¬p
-> ¬s
- 2¬p v r
- 3 r -> ¬t
I- ¬s v ¬t
|
|
101
|
- 1 ¬(m v
n)
- 2 s -> ¬t
- 3 ¬m -> t
I- ¬(s & q)
|
|
102
|
- 1
p->(q<->s)->
- 2 ¬s & m
- 3 p v ¬q
- 4 q & t
I-(¬p &t) v (w &
r)
|
|
|
|
|
103
|
- 1¬(m
& ¬n)
- 2¬(t & ¬u)
- 3 ¬(n &¬p)
- 4 ¬(s & ¬t)
- 5¬(q & ¬r)
- 6¬ (u v w)
- 7 ¬(r &¬s)
- 8 ¬(p &¬q)
I- ¬m
|
|
104
|
- 1 s
-> r
- 2 s v p
- 3 p -> q
- 4 r -> t
I- ¬ q -> t
|
|
105
|
- 1 t -> ¬s
- 2 q -> ¬t
- 3 s v q
I- ¬t
|
|
106
|
- 1
(m&n)-> ¬t
- 2 t v¬s
- 3 ¬ (p v ¬s)
I- ¬(m & n)
|
|
107
|
- 1 ¬ q v s
- 2 ¬s
- 3 ¬(r & s) -> q
I- r
|
|
108
|
- 1 p v¬r
- 2 ¬r -> s
- 3 p -> t
- 4 ¬s
I- t
|
|
109
|
- 1 p-> ¬(s v ¬r)
- 2 q -> ¬(m v r)
- 3 ¬(¬u & ¬p)
- 4 ¬(¬u & ¬q)
I- u
|
|
110
|
- 1 p
-> q
- 2 (p->r) -> (svq)
- 3 (p & q) -> r
- 4 ¬s
I- q
|
|
111
|
- 1 p
-> ¬r
- 2 q -> ¬s
- 3 m -> (r & s)
- 4 n -> (r & s)
- 5 t -> ¬¬m
- 6 ¬t -> ¬¬n
I- ¬p v ¬q
|
|
112
|
- 1 (t & r) <-> s->
- 2 ¬r -> ¬s
I- r
|
|
113
|
- 1 (p v
q) -> r
- 2 w-> ¬(m&s)
- 3 ¬(tvn) ->m
- 4 q <-> t v n->
- 5 s
I- w -> r
|
|
114
|
-
1(p->q) & (r -> s)
- 2 ¬q v ¬s
- 3 ¬(p & r)->t
I- t
|
|
115
|
- 1 ¬(¬q
v ¬t)
- 2 p -> m
- 3 n -> ¬q
- 4 p v n
I- m
|
|
116
|
- 1¬p
-> q
- 2 ¬m -> n
- 3 ¬r -> s
- 4 ¬s -> x
- 5 ¬(¬¬p v ¬¬m)
- 6¬(¬¬r v ¬¬s)
- 7 ¬(s -> ¬q) -> w
- 8¬(n -> ¬x)-> u
I- ¬(¬w v ¬u)
|
|
117
|
- 1
¬(pvq) ->r
- 2 ¬(w v m)
- 3 ¬(z v n)
- 4 ¬(mvn) ->t
- 5 ¬(svp)
- 6 ¬(u vq)
I-¬(¬r v¬t)
|
|
118
|
- 1 p -> w
- 2 q v ¬ w
- 3 ¬( p & q)
I- ¬ p
|
|
119
|
- 1 ¬(p & q)
- 2 ¬r -> q
- 3 ¬p -> r
I- r
|
|
120
|
- 1 p -> q
- 2 ¬ q
- 3 ¬ p -> ( r & s)
I- r & s
|
|
121
|
- 1 p
& q
- 2 r -> ¬q
- 3 ¬r -> s
I- s v¬p
|
|
122
|
- 1 r v s
- 2 ¬t -> ¬p
- 3 r -> ¬q
I- (p & q) -> (s
& t)
|
|
123
|
- 1 q
-> p
- 2 t v s
- 3 q v ¬s
I- ¬(p v r) -> t
|
|
124
|
- 1 p -> q
- 2 (p & q) -> r
- 3 ¬(p & r)
I- ¬p
|
|
125
|
- 1 r -> ¬p
- 2 ¬ (q & ¬r)
I- p -> ¬q
|
|
126
|
- 1(s
& ¬r) -> q
- 2(¬t & ¬q) -> w
- 3 t -> ¬m
- 4 s
- 5 ¬p v ¬q
- 6 ¬(¬m & r)
I- p -> w
|
|
127
|
- 1 ¬m v
p
- 2 q -> m
- 3 x v t
- 4 t -> (r & s)
- 5 ( s & r )->w
I-(¬p->¬q)->(¬w->x)
|
|
128
|
- 1
(p&q)->¬r
- 2 r v (s&t)
- 3 p <-> q->
I- p -> s
|
|
129
|
- 1
p->¬(¬rv¬s)
- 2 ¬¬s ->¬u
- 3 ¬m v n
- 4¬n
- 5 p & q
I-¬(u v m)
|
|
130
|
- 1 t -> m
- 2 ¬(u & p)
- 3 n ->¬m
- 4¬(¬p & ¬w)
- 5 ¬n -> ¬s
- 6 z -> u
- 7 ¬(r v ¬t)
- 8 ¬z -> s
I- w v q
|
|
131
|
- 1 ¬p
-> ¬ s
- 2 ¬p v r
- 3 r -> ¬t
I- ¬s v ¬t
|
|
132
|
- 1 ¬t v ¬r
- 2 ¬r -> p
- 3 ¬(¬r &p)
I- ¬t
|
|
133
|
- 1 r
-> s
- 2 s -> q
- 3 r v (s & t)
I- ¬q -> (t &s)
|
|
134
|
- 1 ¬r
-> s
- 2 s -> (p &q)
- 3 r -> t
- 4 ¬t
I- q
|
|
135
|
- 1 ¬s v ¬r
- 2 ¬r -> ¬t
- 3 ¬p
I- ¬t & ¬p
|
|
136
|
- 1 (r v
q) -> p
- 2 t -> (¬p&¬m)
- 3 t v s
I- r -> s
|
|
137
|
- 1 r
-> n
- 2 t -> (p v r)
- 3 (q v n) -> t
- 4 ¬n
I- ¬p -> ¬q
|
|
138
|
- 1 ¬q
-> ¬(mvt)
- 2 ¬r -> ¬(p&q)
- 3 ¬s -> p
- 4 ¬n-> t
I- ¬(r v s) -> n
|
|
139
|
- 1 p
-> q
- 2 p->(q -> r)
- 3 q->( r -> s)
I- p -> s
|
|
140
|
- 1 ¬p
-> ¬s
- 2¬p v r
- 3 r -> ¬t
I- ¬s v ¬t
|
|
141
|
- 1 ¬(m v
n)
- 2 s -> ¬t
- 3 ¬m -> t
I- ¬(s & q)
|
|
142
|
- 1
p->(q<->s)->
- 2 ¬s & m
- 3 p v ¬q
- 4 q & t
I-(¬p &t)v(w & r)
|
|
143
|
- 1¬(m
& ¬n)
- 2¬(t & ¬u)
- 3 ¬(n &¬p)
- 4 ¬(s & ¬t)
- 5¬(q & ¬r)
- 6¬ (u v w)
- 7 ¬(r &¬s)
- 8 ¬(p &¬q)
I- ¬m
|
|
144
|
-1 ¬q
-> r
-2 t -> ¬ q
-3 ¬ s -> ¬ q
I- t v ¬s -> r
|
|
145
|
1. – ¬(p & q)
2. – p -> r
3. – q v ¬r
I- ¬p
|
|
146
|
1. ¬s v
¬p
2. – q -> ¬r
3. – t -> s & r
I- t -> ¬(p v q)
|
|
147
|
1. – p &¬q
2. – ¬r -> q
3. – r -> s
I- p & s
|
|
148
|
1. – p
& ¬t
2. – s -> t
3. s v q
4. – (q v p)-> u
I- u
|
|
149
|
1. – ¬r
-> s
2. – s -> (p & q)
3. – r -> (t & w)
4. – ¬ t
I- q v (m & n)
|
|
150
|
1.-m->¬
(¬p&¬q)
2. – q -> t
3. – p -> s
I- m -> ¬(¬t & ¬s)
|
|
151
|
1. – p
& ¬q
2. – q v ¬r
3. – p -> ¬s
I- ¬(s v r)
|
|
152
|
1. – (p v q) -> (r&s)
2. – ¬r
I- ¬p
|
|
153
|
1. – p
-> q
2. – q v r
3.-
(r&¬p)->(s&¬p)
4.- ¬q
I- s
|
|
154
|
1.-
¬s->¬(p v ¬t)
2.- t->¬(¬w v ¬n)
3. – ¬s & ¬w
I- m v n
|
|
155
|
1. –
¬(¬mv¬s)
2. – u -> q
3. – t -> ¬q
4. – w -> t
5. – ¬m v w
I- ¬(u & n)
|
|
156
|
1. – p -> q
2. – t -> m
3. – ¬(u &w)
4. – ¬(¬p v ¬z)
5. – ¬r -> ¬q
6. – n -> u
7. – ¬t -> s
8. -¬(m & ¬n)
9. – r -> ¬s
I-¬w
|