Search code examples
formal-methodsz-notation

How to prove (p^q) ^ ( q -> r ) <-> r using Z- notation?

I am trying to prove logical expressions using Z-notations. But, I am new to the Z language. Please help me to prove the above logical expression.

Solution

  • Let's do it using Z notation language which is used as a language for formal specifiaction.

    1st Step : Introduction of Conjunction

    (p ∧ q) ∧ ( q⇒r)  [ ∧ - elim2]

    2nd Step: We will have:

     q ⇒ r

    3rd step: We want get q is true:

    p ∧ q     [ ∧ - elim2]
------
   q

    4th step: Using q and q=>r we can say that r is true.

    For futher information please refer to this book "using Z".