[isabelle] What it means to "embedd logic in Isabelle/HOL", is this a standard procedure?
- To: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>
- Subject: [isabelle] What it means to "embedd logic in Isabelle/HOL", is this a standard procedure?
- From: Alex Meyer <alex153 at outlook.lv>
- Date: Wed, 30 Aug 2017 15:54:09 +0000
- Accept-language: lv-LV, en-US
- Authentication-results: outlook.lv; dkim=none (message not signed) header.d=none; outlook.lv; dmarc=none action=none header.from=outlook.lv;
- Spamdiagnosticmetadata: NSPM
- Spamdiagnosticoutput: 1:99
- Thread-index: AQHTIabth4n55MvyTUmNlqVgCtn9DA==
- Thread-topic: What it means to "embedd logic in Isabelle/HOL", is this a standard procedure?
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>
(* 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