[isabelle] Sequents: meaning of types o, seq', meaning of nonterminals seq, seqobj, seqcont
- To: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>
- Subject: [isabelle] Sequents: meaning of types o, seq', meaning of nonterminals seq, seqobj, seqcont
- From: Alex Meyer <alex153 at outlook.lv>
- Date: Mon, 21 Aug 2017 07:32:33 +0000
- Accept-language: lv-LV, en-US
- Authentication-results: lists.cam.ac.uk; dkim=none (message not signed) header.d=none; lists.cam.ac.uk; dmarc=none action=none header.from=outlook.lv;
- In-reply-to: <HE1P192MB017011B3BCED7031CD3B10DC80860@HE1P192MB0170.EURP192.PROD.OUTLOOK.COM>
- References: <HE1P192MB017011B3BCED7031CD3B10DC80860@HE1P192MB0170.EURP192.PROD.OUTLOOK.COM>
- Spamdiagnosticmetadata: NSPM
- Spamdiagnosticoutput: 1:99
- Thread-index: AQHTGe3RWPFp6WtXPE2Tcxb/e2XAzKKOa0Zb
- Thread-topic: Sequents: meaning of types o, seq', meaning of nonterminals seq, seqobj, seqcont
I am trying to understand https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/Sequents.html and https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/ILL.html and I have problems with the understanding the meaning of the basic items, namely:
types o, seq'
nonterminals seq, seqobj, seqcont?
Do these types and nonterminals have some "real world" counterparts? Sequent is represented by function [o, seq']=>seq', so, maybe o and seq' do not have any real world counterparts?
I am reading "Isabelle's Logics" (especially chapter 4), LNCS 828, Isabelle/Isar reference manual (especially 8.2 and 8.5 about mixfix notations and syntax definition), but I can not grasp the meaning of those symbols and therefor I can not move forward. Any guidance would be very helpful!
I am trying to implement monoidal logic http://www.sciencedirect.com/science/article/pii/S1570868314000573 as a object logic in Isabelle/HOL, but everything is so detached from the "real world" (how the mathematics is being done on paper).
The categorical imperative: Category theory as a ...<http://www.sciencedirect.com/science/article/pii/S1570868314000573>
This article introduces a deontic logic which aims to model the Canadian legal discourse. Category theory is assumed as a foundational framework for logic. A de
Theory ILL (Isabelle2016-1: December 2016)<https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/ILL.html>
Theory ILL theory ILL imports Sequents. (* Title: Sequents/ILL.thy Author: Sara Kalvala and Valeria de Paiva Copyright 1995 University of Cambridge *) theory ILL ...
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