Re: [isabelle] What it means to "embedd logic in Isabelle/HOL", is this a standard procedure?



Hi,

The first step of embedding any language, eg., your logic, in a meta
language, eg., HOL, is the choice of the embedding level.

As far as I know two embedding levels exist in literature: shallow
embedding and deep embedding.

The choice the embedding level depends on what you want to do with your
language.

The best paper that I have for this topic is:
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/11/EmbeddingPaper.pdf

Once you choose your embedding level then you can use the different
Isabelle features to mechanize your logic.

Best,

Yakoub.

2017-08-30 11:54 GMT-04:00 Alex Meyer <alex153 at outlook.lv>:

> I am trying use Isabelle/HOL as logic framework - e.g. to define syntax
> and proof rules as a Isabelle/HOL theory and try to use this theory as
> theorem prover for this logic. There are several works for mechanizing
> linear logic in Isabelle/HOL and I would like to follow them.
>
>
> Is such embedding a standard procedure? E.g. logics usually have standard
> representations - syntax, proof rules. Is there procedure how to encode
> this representation into Isabelle/HOL? I have skimmed through lot of
> tutorials and articles but I have not found tutorial like "how to take
> custome logic, embedd it into Isabelle/HOL and generate theorem prover for
> this logic".
>
>
> Why there is no such tutorial? I guess because there is no such prescribed
> procedore or why else?
>
>
> In http://homepages.inf.ed.ac.uk/ldixon/papers/infrep-06-planill.pdf it
> was said:
>
> "We have formalised ILL (intuitionistic linear logic) as an embedding in
> Isabelle/HOL where both terms and types are HOL datatypes and derivability
> in ILL is defined as membership of an inductively defined set." Can this be
> the universal method for embedding logic?
>
>
> If Isabelle/HOL is so versatile why scientists in field "Universal Logic"
> have not adopted Isabelle/HOL as a platform for managing and developing
> their zoo of logics?
>
>
> There is framework https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/
> library/Sequents/Sequents/Sequents.html that can be used for any logic
> that has sequent calculus. Is this framework useable today? Today
> Isabelle/HOL has Isar and there is not need for inner syntax portion of
> theories but Sequents.thy heavily depends on the inner syntax. What would
> be modern approach for making such framework today for sequent calculus?
>
> Theory Sequents (Isabelle2016-1: December 2016)<https://www.cl.cam.ac.
> uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/Sequents.html>
> www.cl.cam.ac.uk
> (* Title: Sequents/Sequents.thy Author: Lawrence C Paulson, Cambridge
> University Computer Laboratory Copyright 1993 University of Cambridge *)
> section ...
>
>
>



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