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)
   qed

Best!

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

> Does exists a modus tollens rule in isabelle?
>
>


-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
www.inf.pucrs.br/alfio
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.