The L-Framework uses rewrite- and narrowing-based reasoning for proving crucial properties of sequent systems such as admissibility of structural rules, invertibility of rules and cut-elimination. Such procedures have been fully mechanized in Maude, achieving a great degree of automation when used on several sequent systems including intuitionistic and classical logics, linear logic, and normal modal logics.
Structure of the project
The root directory contains the Maude files specifying the different procedures
and analyses. The directory
examples contains case studies including systems
for classical and intuitionistic logic as well as modal and
Further documentation about the procedures implemented is available in the header of each file. See also this paper and its extended version for details on how the properties of sequent systems are encoded as rewriting logic theories.
examples contains several case studies. In each case, the
following files can be found:
logic.maude: defining the syntax and inference rules of the sequent system considered.
prop-XXX.maude: instantiating the different analyses.
exec.maude: Maude file that executes all the analyses.
logic.tex: main LaTeX file importing the output of different analyses.
Running the case studies
Go to the directory of one of the case studies and execute the Maude
interpreter on the file
$> cd examples/g3c $> maude exec.maude \||||||||||||||||||/ --- Welcome to Maude --- /||||||||||||||||||\ Maude 3.0 built: Dec 17 2019 12:08:10 Copyright 1997-2019 SRI International Thu Sep 24 15:33:15 2020 Proof of Height preserving admissibility of weakening on the left ************************************************* Proving the case impR ...... [OK] ...
examples/exec.sh runs all the case studies.
Here the results for the case studies considered so far:
g3c: Two-sided system for classical propositional logic.
g3i: Two-sided, single-conclusion system for intuitionistic propositional logic.
mLJ: Two-sided, multiple-conclusion system for intuitionistic propositional logic.
MALL: One-sided system for multiplicative-additive linear logic.
LL: One-sided system for linear logic (with exponentials)
DyLL: Dyadic system for linear logic
ILL: Intuitionistic Linear Logic
K: Model logic K
S4: Modal logic extending K with the axioms T and 4
KT45: Modal logic extending K with the axioms T,4 and 5. Cut elimination does not hold for this logic
Interested in defining a new case study?
See this step-by-step tutorial explaining how to define a sequent system and prove its properties.