*To*: Oleksandr Gavenko <gavenkoa at gmail.com>*Subject*: Re: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Mon, 21 May 2012 09:47:53 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <87bolia9gu.fsf@desktop.home.int>*References*: <87havcyn5p.fsf@desktop.home.int> <CANofLe+qNjhzCpQP41OE+dLh8LLPAZpXRN8YezngkygnoOWL+Q@mail.gmail.com> <87bolia9gu.fsf@desktop.home.int>

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

**Follow-Ups**:

**References**:**[isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?***From:*Oleksandr Gavenko

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

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

- Previous by Date: Re: [isabelle] Proof mode maintained after outcommenting [Re: Isabelle2012-RC3 available for testing]
- Next by Date: Re: [isabelle] isabelle2012-rc3\isabelle.exe removed by Norton when executed
- Previous by Thread: Re: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?
- Next by Thread: Re: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?
- Cl-isabelle-users May 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list