# [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;
• References: <HE1P192MB017011B3BCED7031CD3B10DC80860@HE1P192MB0170.EURP192.PROD.OUTLOOK.COM>
• Spamdiagnosticoutput: 1:99
• Thread-topic: 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 ...

```

• Follow-Ups:

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.