isabelle: src/Sequents/README.html@05d5615e12d3 (annotated)

15283 f21466450330 DOCTYPE declaration added webertj parents: 5383 diff changeset	1	<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
f21466450330 DOCTYPE declaration added webertj parents: 5383 diff changeset	2
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	3	<!-- $Id$ -->
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	4
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	5	<HTML>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	6
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	7	<HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	8	<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	9	<TITLE>Sequents/README</TITLE>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	10	</HEAD>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	11
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	12	<BODY>
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	13
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	14	<H2>Sequents: Various Sequent Calculi</H2>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	15
3279 815ef5848324 tuned all READMEs; wenzelm parents: 2073 diff changeset	16	This directory contains the ML sources of the Isabelle system for
815ef5848324 tuned all READMEs; wenzelm parents: 2073 diff changeset	17	various Sequent, Linear, and Modal Logic.<p>
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	18
3279 815ef5848324 tuned all READMEs; wenzelm parents: 2073 diff changeset	19	The subdirectories <tt>ex</tt>, <tt>ex/LK</tt>, <tt>ex/ILL</tt>,
815ef5848324 tuned all READMEs; wenzelm parents: 2073 diff changeset	20	<tt>ex/Modal</tt> contain some examples.<p>
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	21
3279 815ef5848324 tuned all READMEs; wenzelm parents: 2073 diff changeset	22	Much of the work in Modal logic was done by Martin Coen. Thanks to
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	23	Rajeev Gore' for supplying the inference system for S43. Sara Kalvala
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	24	reorganized the files and supplied Linear Logic. Jacob Frost provided
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	25	some improvements to the syntax of sequents.
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	26
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	27	<P>Useful references on sequent calculi:
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	28
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	29	<UL>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	30	<LI>Steve Reeves and Michael Clarke,<BR>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	31	Logic for Computer Science (Addison-Wesley, 1990)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	32	<LI>G. Takeuti,<BR>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	33	Proof Theory (North Holland, 1987)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	34	</UL>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	35
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	36	Useful references on Modal Logics:
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	37	<UL>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	38	<LI>Melvin C Fitting,<BR>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	39	Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	40
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	41	<LI>Lincoln A. Wallen,<BR>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	42	Automated Deduction in Nonclassical Logics (MIT Press, 1990)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	43	</UL>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	44
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	45	Useful references on Linear Logic:
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	46	<UL>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	47	<LI>A. S. Troelstra<BR>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	48	Lectures on Linear Logic (CSLI, 1992)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	49
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	50	<LI>S. Kalvala and V. de Paiva<BR>
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	51	Linear Logic in Isabelle (in TR 379, University of Cambridge
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	52	Computer Lab, 1995, ed L. Paulson)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	53	</UL>
5383 74c2da44d144 weblinted, tuned; wenzelm parents: 3279 diff changeset	54
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	55	</BODY></HTML>

author	wenzelm
	Sat, 14 Feb 2009 22:58:30 +0100
changeset 29738	05d5615e12d3
parent 15582	7219facb3fd0
child 36862	952b2b102a0a
permissions	-rw-r--r--