Email Gateway (Aug 22 2022 at 15:53): Email Gateway (Aug 22 2022 at 15:53):From: Alex Meyer <alex153@outlook.lv>
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 ...
Email Gateway (Aug 22 2022 at 15:55):From: Lawrence Paulson <lp15@cam.ac.uk>
Sequents, which are lists of formulas, are represented using a trick due to G Huet. The point is to obtain associative unification for free from higher-order unification. I’m afraid I don’t recall many other details: this is 25-year-old work. There are some details in section 3.7 of the Logics manual.
However, not all types need to have "real world interpretations”.
Larry Paulson
Last updated: Apr 24 2024 at 04:17 UTC