Re: [isabelle] The difference between /\ , â and -> , =>



This is a fundamental question about Isabelle as a logical framework. Isabelle provides general inference mechanisms for combining proofs and for proving not just simple statements, but what are essentially inference rules. This requires a form of universal quantification and a form of implication that operate outside the level of logical assertions.

The advantage of having separate symbols can be seen when comparing Isabelle proofs with those done in other implementations of higher-order logic. Let suppose that you have proved the theorem

	P(x,y) ==> Q(y) ==> P (x, f x).

With Isabelle, the quantification over x and y and the implications for P and Q are dealt with automatically, whether you use this âforwardsâ or âbackwardsâ. But in a traditional HOL system, youâll devote effort to removing the quantifiers and reasoning with the implications. And the difference is even greater when you use or derive specialist induction rules.

Larry Paulson


> On 9 Feb 2015, at 10:39, mahmoud abdelazim <m.abdelazim at icloud.com> wrote:
> 
> What is the difference in Isabelle between Universal Quantification /\ and â ?
> What is the difference in Isabelle between the implications   =>  and ->  ?





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