A Harder Example
(PvQ)>R
-[(P>R)&(Q>R)]
(PvQ)>R | (P>R)&(Q>R)
A Harder Example
(PvQ)>R
-[(P>R)&(Q>R)]
(PvQ)>R | (P>R)&(Q>R)
A Harder Example
(-&) Rule
-(A&B)
-A
-B
(PvQ)>R
-[(P>R)&(Q>R)]
(PvQ)>R | (P>R)&(Q>R)
A Harder Example
(-&) Rule
-(A&B)
-A
-B
(PvQ)>R
1 -[(P>R)&(Q>R)]
-(P>R)
-(Q>R)
(PvQ)>R | (P>R)&(Q>R)
A Harder Example
(PvQ)>R
1 -[(P>R)&(Q>R)]
-(P>R)
-(Q>R)
(PvQ)>R | (P>R)&(Q>R)
A Harder Example
(->) Rule
-(A>B)
A
-B
(PvQ)>R
1 -[(P>R)&(Q>R)]
-(P>R)
-(Q>R)
(PvQ)>R | (P>R)&(Q>R)
A Harder Example
(PvQ)>R
1 -[(P>R)&(Q>R)]
(->) Rule
-(A>B)
A
-B
2
-(P>R)
P
-R
-(Q>R)
(PvQ)>R | (P>R)&(Q>R)
A Harder Example
(PvQ)>R
1 -[(P>R)&(Q>R)]
(->) Rule
-(A>B)
A
-B
2
-(P>R)
P
-R
-(Q>R)
(PvQ)>R | (P>R)&(Q>R)
A Harder Example
(PvQ)>R
1 -[(P>R)&(Q>R)]
(->) Rule
-(A>B)
A
-B
2
-(P>R) 3 -(Q>R)
P
Q
-R
-R
(PvQ)>R | (P>R)&(Q>R)
A Harder Example
(PvQ)>R
1 -[(P>R)&(Q>R)]
2
-(P>R) 3 -(Q>R)
P
Q
-R
-R
(PvQ)>R | (P>R)&(Q>R)
(>) Rule
A Harder Example
A>B
-A
(PvQ)>R
1 -[(P>R)&(Q>R)]
B
2
-(P>R) 3 -(Q>R)
P
Q
-R
-R
(PvQ)>R | (P>R)&(Q>R)
(>) Rule
A Harder Example
A>B
-A
(PvQ)>R
1 -[(P>R)&(Q>R)]
(PvQ)>R | (P>R)&(Q>R)
B
2
-(P>R) 3 -(Q>R)
P
Q
-R
-R
THE RESULT OF APPLYING
A RULE MUST APPEAR ON
EVERY OPEN BRANCH BELOW
THE PLACE IT IS APPLIED.
(>) Rule
A Harder Example
A>B
-A
4 (PvQ)>R
1 -[(P>R)&(Q>R)]
(PvQ)>R | (P>R)&(Q>R)
B
2
-(P>R) 3 -(Q>R)
P
Q
-R
-R
-(PvQ) R
-(PvQ) R
THE RESULT OF APPLYING
A RULE MUST APPEAR ON
EVERY OPEN BRANCH BELOW
THE PLACE IT IS APPLIED.
A Harder Example
4 (PvQ)>R
1 -[(P>R)&(Q>R)]
2
-(P>R) 3 -(Q>R)
P
Q
-R
-R
-(PvQ) R
*
-(PvQ) R
*
(PvQ)>R | (P>R)&(Q>R)
A Harder Example
4 (PvQ)>R
1 -[(P>R)&(Q>R)]
2
-(P>R) 3 -(Q>R)
P
Q
-R
-R
-(PvQ) R
*
-(PvQ) R
*
(PvQ)>R | (P>R)&(Q>R)
A Harder Example
4 (PvQ)>R
1 -[(P>R)&(Q>R)]
2
(-v) Rule
-(AvB)
-A
-B
-(P>R) 3 -(Q>R)
P
Q
-R
-R
-(PvQ) R
*
-(PvQ) R
*
(PvQ)>R | (P>R)&(Q>R)
A Harder Example
4 (PvQ)>R
1 -[(P>R)&(Q>R)]
2
(-v) Rule
-(P>R) 3 -(Q>R)
P
Q
-R
-R
-(AvB) 5 -(PvQ) R
-P
-A
*
-Q
-B
-(PvQ) R
*
(PvQ)>R | (P>R)&(Q>R)
A Harder Example
4 (PvQ)>R
1 -[(P>R)&(Q>R)]
2
(-v) Rule
-(P>R) 3 -(Q>R)
P
Q
-R
-R
-(AvB) 5 -(PvQ) R
-P
-A
*
-Q
-B
-(AvB) =
-A&-B
-(PvQ) R
*
(PvQ)>R | (P>R)&(Q>R)
A Harder Example
4 (PvQ)>R
1 -[(P>R)&(Q>R)]
2
(-v) Rule
-(P>R) 3 -(Q>R)
P
Q
-R
-R
-(AvB) 5 -(PvQ) R
-P
-A
*
-Q
-B
-(PvQ) R
*
(PvQ)>R | (P>R)&(Q>R)
A Harder Example
4 (PvQ)>R
1 -[(P>R)&(Q>R)]
2
(-v) Rule
-(P>R) 3 -(Q>R)
P
Q
-R
-R
-(AvB) 5 -(PvQ) R 6 -(PvQ) R
-P
-P
-A
*
*
-Q
-Q
-B
(PvQ)>R | (P>R)&(Q>R)
A Harder Example
4 (PvQ)>R
1 -[(P>R)&(Q>R)]
2
-(P>R) 3 -(Q>R)
P
Q
-R
-R
5 -(PvQ) R 6 -(PvQ) R
-P
-P
*
*
-Q
-Q
*
*
(PvQ)>R | (P>R)&(Q>R)
A Harder Example
4 (PvQ)>R
1 -[(P>R)&(Q>R)]
2
-(P>R) 3 -(Q>R)
P
Q
-R
-R
5 -(PvQ) R 6 -(PvQ) R
-P
-P
*
*
-Q
-Q
*
*
(PvQ)>R | (P>R)&(Q>R)
VALID
Ordering Strategy
It is best to do non-branching steps first.
For more click here

A Harder Example