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


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

The best paper that I have for this topic is:

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



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

> 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 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
> 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)<
> uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/Sequents.html>
> (* 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.