Re: [isabelle] modus tollens rule in isabelle

Hi Mahmoud,

Like Peter mentioned,  you can prove it if you want. There are many ways.
Two of them are shown below:

theorem mt:
   assumes mj:  "AâB" and mi: "ÂB"
   shows "ÂA" using mj and mi by simp

theorem mt2:
assumes mj:  "AâB" and mi: "ÂB"
   shows "ÂA"
    proof (rule notI)
      assume A
      from mj and this  have B by (rule mp)
      from mi and this show False by (rule notE)


On Fri, Feb 27, 2015 at 3:13 PM, mahmoud abdelazim <m.abdelazim at>

> Does exists a modus tollens rule in isabelle?

Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica
90619-900 -Porto Alegre - RS - Brasil

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.