This directory (isabelle/2005/seqms) contains cut elimination results,
ultimately for the sequent system GLS, see theorem glss_ca in theory glca
This work is described in the paper
Jeremy E. Dawson & Rajeev GorĂ©,
Generic Methods for Formalising Sequent Calculi Applied to Provability Logic.
In Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2010),
LNCS 6397, 263-277.
The theories pmg... contain material related to establishing that you can
define a lattice based on certain axioms - run
open pm0_class ; open pm_ge0_class ;
with definitions
"pg_join ?c ?d == ?c + (?d - ?c)"
"pg_meet ?c ?d == ?c - (?c - ?d)"
prove these are lub, glb, by
pg_join_le1, pg_join_le2, pg_meet_le1, pg_meet_le2, pg_meet_glb, pg_join_lub
We also have cut-admissibility for lksss (theorem lks_scas_all in theory calks)
Also contains material for S4 and S4.3, with Jesse Wu
Also contains material for S4C and GTD (from Mints at Jaegerfest, Dec 2013)
Also contains material for CK + {T,D,4}, constructive modal logic,
theories ipl, ipldt, lctr - this is work in progress,
need to deal with left contraction admissibility - see lctr.thy
and left weakening admissibility - see wk_adm_antec in ctr.thy
Mon Jun 5 14:27:44 AEST 2017 - split gentree into gentree and gcmctree