Re: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?



Normally, if you want to perform deductions that involve a set of assumptions, as the deduction theorem allows, you formalise a sequent calculus or alternatively a natural deduction system, of which several examples are already distributed with Isabelle.

Most of our recent documentation focuses on how to use Isabelle/HOL, which is possibly not relevant to your application. What sort of calculus do you want to formalise, And with what application in mind?

Larry Paulson


On 20 May 2012, at 21:22, Oleksandr Gavenko wrote:

> I want to notice that proofs in 'Pure' also is not convenient.
> For example without deduction theorem I need make a lot of rut work...






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