isabelle: src/Sequents/ROOT@e0755162093f (annotated)

51397 03b586ee5930 support for 'chapter' specifications within session ROOT; wenzelm parents: 48738 diff changeset	1	chapter Sequents
03b586ee5930 support for 'chapter' specifications within session ROOT; wenzelm parents: 48738 diff changeset	2
48738 f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default; wenzelm parents: 48483 diff changeset	3	session Sequents = Pure +
69319 baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb; wenzelm parents: 69272 diff changeset	4	description "
48475 02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	5	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	6	Copyright 1991 University of Cambridge
02dd825f5a4e more session ROOT files; wenzelm parents: diff changeset	7
51403 2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	8	Various Sequent Calculi for Classical, Linear, and Modal Logic.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	9
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	10	Much of the work in Modal logic was done by Martin Coen. Thanks to Rajeev
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	11	Gore' for supplying the inference system for S43. Sara Kalvala reorganized
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	12	the files and supplied Linear Logic. Jacob Frost provided some improvements
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	13	to the syntax of sequents.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	14
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	15
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	16	Useful references on sequent calculi:
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	17
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	18	Steve Reeves and Michael Clarke, Logic for Computer Science
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	19	(Addison-Wesley, 1990)
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	20
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	21	G. Takeuti, Proof Theory (North Holland, 1987)
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	22
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	23
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	24	Useful references on Modal Logics:
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	25
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	26	Melvin C Fitting, Proof Methods for Modal and Intuitionistic Logics
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	27	(Reidel, 1983)
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	28
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	29	Lincoln A. Wallen, Automated Deduction in Nonclassical Logics (MIT Press,
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	30	1990)
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	31
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	32
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	33	Useful references on Linear Logic:
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	34
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	35	A. S. Troelstra, Lectures on Linear Logic (CSLI, 1992)
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	36
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	37	S. Kalvala and V. de Paiva, Linear Logic in Isabelle (in TR 379, University
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index; wenzelm parents: 51397 diff changeset	38	of Cambridge Computer Lab, 1995, ed L. Paulson)
69319 baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb; wenzelm parents: 69272 diff changeset	39	"
70675 efd995488228 declare session directories; wenzelm parents: 69319 diff changeset	40	directories "LK"
48483 9bfb6978eb80 more explicit document = false to reduce warnings; wenzelm parents: 48475 diff changeset	41	theories
9bfb6978eb80 more explicit document = false to reduce warnings; wenzelm parents: 48475 diff changeset	42	LK
9bfb6978eb80 more explicit document = false to reduce warnings; wenzelm parents: 48475 diff changeset	43	ILL
9bfb6978eb80 more explicit document = false to reduce warnings; wenzelm parents: 48475 diff changeset	44	ILL_predlog
9bfb6978eb80 more explicit document = false to reduce warnings; wenzelm parents: 48475 diff changeset	45	Washing
9bfb6978eb80 more explicit document = false to reduce warnings; wenzelm parents: 48475 diff changeset	46	Modal0
9bfb6978eb80 more explicit document = false to reduce warnings; wenzelm parents: 48475 diff changeset	47	T
9bfb6978eb80 more explicit document = false to reduce warnings; wenzelm parents: 48475 diff changeset	48	S4
9bfb6978eb80 more explicit document = false to reduce warnings; wenzelm parents: 48475 diff changeset	49	S43
55229 08f2ebb65078 simplified sessions; wenzelm parents: 51403 diff changeset	50	(* Examples for Classical Logic *)
08f2ebb65078 simplified sessions; wenzelm parents: 51403 diff changeset	51	"LK/Propositional"
08f2ebb65078 simplified sessions; wenzelm parents: 51403 diff changeset	52	"LK/Quantifiers"
08f2ebb65078 simplified sessions; wenzelm parents: 51403 diff changeset	53	"LK/Hard_Quantifiers"
08f2ebb65078 simplified sessions; wenzelm parents: 51403 diff changeset	54	"LK/Nat"

author	immler
	Sun, 03 Nov 2019 21:46:46 -0500
changeset 71034	e0755162093f
parent 70675	efd995488228
child 75992	1f6d79b62222
permissions	-rw-r--r--