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?
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