Email Gateway (Aug 22 2022 at 15:57): Email Gateway (Aug 22 2022 at 15:57):From: Alex Meyer <alex153@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 ...
Email Gateway (Aug 22 2022 at 15:57):From: Nemouchi Yakoub <y.nemouchi@gmail.com>
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.
Last updated: May 06 2024 at 20:16 UTC