View on GitHub


This tool aims at developing techniques for proving structural properties of sequent systems using rewriting logic (Maude)

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.

Getting started

The project was tested in Maude 3.0. No extra library is needed for execution. The tool produces LaTeX files with the results.

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 substructural logics.


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.

Case Studies

The directory examples contains several case studies. In each case, the following files can be found:

Running the case studies

Go to the directory of one of the case studies and execute the Maude interpreter on the file exec.maude:

$> 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]

The bash examples/ runs all the case studies.


Here the results for the case studies considered so far:

Interested in defining a new case study?

See this step-by-step tutorial explaining how to define a sequent system and prove its properties.