[isabelle] Sequents: meaning of types o, seq', meaning of nonterminals seq, seqobj, seqcont



Hello!


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>
www.sciencedirect.com
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>
www.cl.cam.ac.uk
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>
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.