Re: [isabelle] Is it possible to prove meta-theorem of deduction in Isabelle for propositional logic?
On 2012-05-20, Randy Pollack wrote:
> You can do meta logic of "deeply embedded" formal systems. Define the
> syntax and derivations of your object system as datatypes and
> inductive relations in (for example) isabelle HOL. Then you have the
> power of induction over these representations.
Firstly thanks to Larry Paulson and Randy Pollack for answer...
I understand idea about "induction over these representations", and will try
to learn more on Isabelle to realise this idea...
> However reasoning _within_ such deeply embedded systems is not vey
> convenient unless you put effort into building tools.
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...
I as say that I am newbie for Isabelle and so I do not understand what you
mean by saying "building tools"... Can you explain more? Is this mean to write
some SML support code?
> Propositional logic should be simple. If your object system has
> binding, look into using nominal isabelle. There are many examples of
> reasoning about formalized object systems.
By saying "nominal isabelle" do you mean:
I would glad if someone point me for examples of "reasoning about formalized
object systems" as I new to this field and don't know from what to start...
This archive was generated by a fusion of
Pipermail (Mailman edition) and