propositional theorems
- by gcc
wang's theorem to prove theorems in propositonal calculus
Label Sequent Comment
S1: P ? Q, Q ? R, ¬R ? ¬P Initial sequent.
S2: ¬P ? Q, ¬Q ? R, ¬R ? ¬P Two applications of R5.
S3: ¬P ? Q, ¬Q ? R ? ¬P, R Rl.
S4: ¬P, ¬Q ? R ? ¬P, R S4 and S5 are obtained from S3 with
R3. Note that S4 is an axiom since P
appears on both sides of the sequent ar-
row at the top level.
S5: Q, ¬Q ? R ? ¬P, R The other sequent generated by the ap-
plication of R3.
S6: Q, ¬Q ? ¬P, R S6 and S7 are obtained from S5 using
R3.
S7: Q, R ? ¬P, R This is an axiom.
S8: Q ? ¬P, R, Q Obtained from S6 using R1. S8 is an
axiom. The original sequent is now
proved, since it has successfully been
transformed into a set of three axioms
with no unproved sequents left over.
//R1,R2,R3,R4,R5 is transformation
myhomework is so complicate as you can see and i must finish homework in 4 days
i just want help ,can you show me how i should construct the algorithm or how i should
take and store the input