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



We have a paper in LPAR 2010 (Dawson & Gore) which gives a couple of pages on deep embeddings, what (we think) that means, etc. Email me if you want me to send you a copy.

The comment that

reasoning _within_ such deeply embedded systems is not vey
convenient unless you put effort into building tools

reflects the fact that instead of proving something, you are proving that it is provable. Fortunately the extra effort is just repetitive grunt work for which Isabelle's SML user interface is ideally suited.  Unfortunately you will no doubt have been led to believe that the SML user interface is not the way to go in using Isabelle.

Cheers,

Jeremy



Oleksandr Gavenko wrote:
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:

  http://isabelle.in.tum.de/nominal/  ??

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