Index of /ports/math/isabelle/work/Isabelle2005/src/Sequents

 Name                    Last modified       Size  Description

 Parent Directory        09-Aug-2008 06:09      -  
 ILL.ML                  18-Sep-2005 06:20     4k  
 ILL.ML.html             09-Aug-2008 06:10     0k  
 ILL.thy                 18-Sep-2005 06:20     3k  
 ILL.thy.html            09-Aug-2008 06:10     0k  
 ILL/                    09-Aug-2008 06:10      -  
 IsaMakefile             27-Jul-1999 10:02     1k  
 IsaMakefile.html        09-Aug-2008 06:10     4k  
 LK.thy                  18-Sep-2005 06:20     1k  
 LK.thy.html             09-Aug-2008 06:10     0k  
 LK/                     09-Aug-2008 06:10      -  
 LK0.ML                  18-Sep-2005 06:20     5k  
 LK0.ML.html             09-Aug-2008 06:10     0k  
 LK0.thy                 18-Sep-2005 06:20     4k  
 LK0.thy.html            09-Aug-2008 06:10     0k  
 Modal/                  09-Aug-2008 06:10      -  
 Modal0.ML               18-Sep-2005 06:20     1k  
 Modal0.ML.html          09-Aug-2008 06:10     0k  
 Modal0.thy              18-Sep-2005 06:20     1k  
 Modal0.thy.html         09-Aug-2008 06:10     0k  
 ROOT.ML                 18-Sep-2005 06:20     1k  
 ROOT.ML.html            09-Aug-2008 06:10     0k  
 S4.ML                   18-Sep-2005 06:20     1k  
 S4.ML.html              09-Aug-2008 06:10     0k  
 S4.thy                  18-Sep-2005 06:20     1k  
 S4.thy.html             09-Aug-2008 06:10     0k  
 S43.ML                  18-Sep-2005 06:20     1k  
 S43.ML.html             09-Aug-2008 06:10     0k  
 S43.thy                 18-Sep-2005 06:20     3k  
 S43.thy.html            09-Aug-2008 06:10     0k  
 Sequents.thy            18-Sep-2005 06:20     4k  
 Sequents.thy.html       09-Aug-2008 06:10     0k  
 T.ML                    18-Sep-2005 06:20     1k  
 T.ML.html               09-Aug-2008 06:10     0k  
 T.thy                   18-Sep-2005 06:20     1k  
 T.thy.html              09-Aug-2008 06:10     0k  
 modal.ML                27-Jul-1999 10:00     3k  
 modal.ML.html           09-Aug-2008 06:10     0k  
 prover.ML               17-Jun-2005 09:35     7k  
 prover.ML.html          09-Aug-2008 06:10     0k  
 simpdata.ML             18-Sep-2005 06:20     9k  
 simpdata.ML.html        09-Aug-2008 06:10     0k

Sequents/README

Sequents: Various Sequent Calculi

This directory contains the ML sources of the Isabelle system for various Sequent, Linear, and Modal Logic.

The subdirectories ex, ex/LK, ex/ILL, ex/Modal contain some examples.

Much of the work in Modal logic was done by Martin Coen. Thanks to Rajeev Gore' for supplying the inference system for S43. Sara Kalvala reorganized the files and supplied Linear Logic. Jacob Frost provided some improvements to the syntax of sequents.

Useful references on sequent calculi:

Steve Reeves and Michael Clarke,
Logic for Computer Science (Addison-Wesley, 1990)
G. Takeuti,
Proof Theory (North Holland, 1987)

Useful references on Modal Logics:

Melvin C Fitting,
Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983)
Lincoln A. Wallen,
Automated Deduction in Nonclassical Logics (MIT Press, 1990)

Useful references on Linear Logic:

A. S. Troelstra
Lectures on Linear Logic (CSLI, 1992)
S. Kalvala and V. de Paiva
Linear Logic in Isabelle (in TR 379, University of Cambridge Computer Lab, 1995, ed L. Paulson)