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

author	nipkow
	Tue, 21 Dec 2010 08:38:03 +0100
changeset 41341	e65a122057ad
parent 36862	952b2b102a0a
permissions	-rw-r--r--