isabelle: src/Sequents/README.html@56187238220d (annotated)

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

author	paulson
	Mon, 08 May 2000 16:59:02 +0200
changeset 8835	56187238220d
parent 5383	74c2da44d144
child 15283	f21466450330
permissions	-rw-r--r--