Structural Proof Theory in Maude

`General Information`

General and effective methods are required for providing good automation strategies to prove properties of sequent systems. Structural properties such as admissibility, invertibility, and permutability of rules are crucial in proof theory, and they can be used for proving other properties such as cut-elimination. However, finding proofs for these properties require inductive reasoning over the provability relation, which is often quite elaborated, exponentially exhaustive, and error prone. This tool aims at developing techniques for proving structural properties of sequent systems. The proposed techniques are presented in the rewriting logic metalogical framework, and use rewrite- and narrowing-based reasoning. They have been fully mechanized in Maude and have achieved a great degree of automation when used on several sequent systems including propositional intuitionistic and classical logic, multi-conclusion intuitionistic logic, propositional linear logic, and the normal modal logics K and S4.

See [OPR18] for further details.

`Download`

The code was implemented in Maude and tested in the version 2.7. Take a look at the header of the files for further details and examples:

meta-level-ext.maude: some extra functionalities for the meta-level.
theorem-proving.maude: algorithms for proving sequent system properties.
test_g3ip.maude: tests for intuitionistic propositional logic.
test_mlj.maude: tests for multiconclusion intuitionistic propositional logic.
test_g3cp.maude: tests for propositional classical logic.
test_llM.maude: tests for the monadic system of propositional linear logic.
test_llD.maude: tests for the dyadic system of propositional linear logic.
test_modalK.maude: tests for the modal logics K and S4.

Download

`Examples`

In the tabs above, we explain the results for different logical systems: propositional intuitionistic logic (G3ip), multiple conclusion propositional intuitionistic logic (mLJ), propositional classical logic (G3c), the dyadic and the monadic systems for propositional linear logic, and the normal modal logics K and S4.

`References`

[ OPR18 ]

C. Olarte, E. Pimentel and C. Rocha: Proving Structural Properties of Sequent Systems in Rewriting Logic. Submitted to WRLA'18 (PDF).

`Contact`

For further information, please contact the authors of [OPR18]: Carlos Olarte, Elaine Pimentel or Camilo Rocha .

`Systems for Propositional Intuitionistic Logic`

In this series of examples we prove properties of two different systems for intuitionistic propositional logic : Gentzen's G3ip system and Maehara's multi-conclusion system (mLJ).

`System G3ip`

The tests can be run as follows:

maude test_g3ip.maude

In this file, we first establish the syntax of propositional logic.

fmod SYNTAX is
    pr NAT .
    sort Prop . --- Atomic propositions
    sort Formula . --- Formulas 
    subsort Prop < Formula .
    
    --- Atomic Propositions
    ops p  : Nat -> Prop [ctor] .
    --- Conjunction
    op _/\_ : Formula Formula -> Formula [ctor assoc prec 30] .
    --- Disjunction
    op _\/_ : Formula Formula -> Formula [ctor assoc prec 30] .
    --- False
    op False : -> Formula [ctor] .
    --- True
    op True : -> Formula [ctor] .
    --- Implication
    op _-->_ : Formula Formula -> Formula [ctor prec 35] .

    --- Set of Formulas
    sort SFormula . 
    subsort Formula < SFormula .
    op * : -> SFormula . *** empty set of formulas
    op _;_ : SFormula SFormula -> SFormula [prec 40 ctor assoc comm id: * ] .
endfm

fmod SEQUENT is
    pr SYNTAX .
    inc OBJ-LOGIC .
    --- Constructor for sequents .
    op _|-_ : SFormula Formula -> Sequent [ctor prec 50 format(b o r o )] .
endfm

Then we define the inference rules of the system.

mod G3i is
    pr SEQUENT .
    pr META-LEVEL .
    var P : Prop .
    vars F G H : Formula .
    vars C C' : SFormula .
    --- A new "fresh" constant
    op ANY : -> SFormula .
    
    rl [I] : P ; C  |- P => proved .
    rl [AndL] : F /\ G ; C |- H => F ; G ; C |- H .
    rl [AndR] : C |- F /\ G => (C |- F) , (C |- G) .
    rl [botL] : C ; False |- H => proved .
    rl [topR] : C |- True => proved .
    rl [topL] : C ; True |- G => C |- G .
    rl [OrL] : C ; F \/ G |- H => (C ; F |- H) , (C ; G |- H) .
    rl [OrR1] : C |- F \/ G =>  C |- F .
    rl [OrR2] : C |- F \/ G =>  C |- G .
    rl [ImpR] : C |- F --> G =>  C ; F |- G .
    rl [ImpL] : C ; F --> G |- H => (C ; F --> G |- F) , (C ; G |- H) .
endm

The next step is to define an instance of the theory TH-INPUT (see file theorem-proving.maude). Such instance contains the rules we want to prove admissible and also it may contain a list of theorems that were already proved (and can be used during proofs). In the first test, we specify:

two rules to be proved to be admissible: weakening, contraction;
one theorem stating the invertibility of the right premiss of the implication left rule;
no previous theorem is assumed and none of the rules is assumed (a priori) invertible.

mod G3i-TEST is
    inc G3i .
    pr META-LEVEL .
    ops modName seqType : -> Qid .
    eq modName = 'G3i .
    op knownTheorems : -> RuleSet .
    eq knownTheorems = none .
    op knownInvRules : -> QidList .
    eq knownInvRules = nil .

    --- Weakening
    op Th-Weakening : -> Rule .
    eq Th-Weakening = ( rl '_|-_['C:SFormula,'F:Formula] => '_|-_['_;_['C:SFormula,'ANY.SFormula],'F:Formula] [ label('Th-Weakening) ]. ) .
    --- Contraction
    op Th-Contraction : -> Rule .
    eq Th-Contraction = ( rl '_|-_['_;_['C:SFormula,'C:SFormula],'F:Formula] => '_|-_['C:SFormula,'F:Formula] [ label('Th-Contraction) ]. ) .

    --- Inv of implication on the right premiss (if Gamma, A->B |-C  then Gamma, B |-C )
    op Th-Imp : -> Rule .
    eq Th-Imp = ( rl '_|-_['_;_['C:SFormula,'_-->_['F:Formula,'G:Formula]],'H:Formula] => '_|-_['_;_['C:SFormula,'G:Formula],'H:Formula] [ label('Th-Implication) ]. ) .
endm

Using this specification, we can prove the following:

select THEOREM-PROVING-G3i .
red invertibility . 
result Result: {'AndL ; true}
{'AndR ; true}
{'I ; true}
{'ImpL ; false}
{'ImpR ; false}
{'OrL ; true}
{'OrR1 ; false}
{'OrR2 ; false}
{'botL ; true}
{'topL ; true}
{'topR ; true}

We note that the prover is not able to show that implication right (ImpR) is invertible. For that, we first need to prove that weakening is admissible:

red admissible?(Th-Weakening) .
result Bool: true

The result for the other two theorems is the following:

red admissible?(Th-Imp) . --- invertibility of the right premiss of the implication left rule
result Bool: true
red admissible?(Th-Contraction) .
result Bool: false

We note that contraction is indeed admissible in G3ip. However, that proof requires the invertibility lemmas.

`System G3ip + Weakening`

We already proved that the rule Weakening is admissible in G3ip. The module G3iW adds to G3i the rule for weakening:

rl [W] : C ; C' |- G => C |- G .

In this new system, we can prove the rule for implication right to be invertible:

select THEOREM-PROVING-G3iW  .
red invertibility .
{'AndL ; true}
{'AndR ; true}
{'I ; true}
{'ImpL ; false}
{'ImpR ; true}
{'OrL ; true}
{'OrR1 ; false}
{'OrR2 ; false}
{'W ; false}
{'botL ; true}
{'topL ; true}
{'topR ; true}

Weakening, of course, is not invertible.

`System G3ip + Weakening + Invertibilities`

Finally, we can conclude the proof of admissibility of contraction by assuming weakening and the previous theorems about invertibility. This is done in the module G3iInv-TEST.

--- All the already proved invertibility theorems are assumed
mod G3iInv-TEST is
    inc G3i .
    pr META-LEVEL .
    ops modName seqType : -> Qid .
    eq modName = 'G3i .
    op knownTheorems : -> RuleSet .
    eq knownTheorems = Th-Imp .
    op knownInvRules : -> QidList .
    eq knownInvRules = 'OrL 'AndL 'AndR 'topL 'topR 'botL 'ImpR .
    --- Theorem about implication (if Gamma, A->B |-C  then Gamma, B |-C )
    op Th-Imp : -> Rule .
    eq Th-Imp = ( rl '_|-_['_;_['C:SFormula,'_-->_['F:Formula,'G:Formula]],'H:Formula] => '_|-_['_;_['C:SFormula,'G:Formula],'H:Formula] [ label('Th-Implication) ]. ) .
    --- Contraction
    op Th-Contraction : -> Rule .
    eq Th-Contraction = ( rl '_|-_['_;_['C:SFormula,'C:SFormula],'F:Formula] => '_|-_['C:SFormula,'F:Formula] [ label('Th-Contraction) ]. ) .
endm

In this system, we can prove contraction to be admissible:

select THEOREM-PROVING-G3iInv .
red admissible?(Th-Contraction) .
result Bool: true

Moreover, we can analyze the permutation of rules:

red analyzePermutation .

{{'AndL ; 'AndL ; true}}
{{'AndL ; 'AndR ; true}}
{{'AndL ; 'I ; true}}
{{'AndL ; 'ImpL ; true}}
{{'AndL ; 'ImpR ; true}}
{{'AndL ; 'OrL ; true}}
{{'AndL ; 'OrR1 ; true}}
{{'AndL ; 'OrR2 ; true}}
{{'AndL ; 'botL ; true}}
{{'AndL ; 'topL ; true}}
{{'AndL ; 'topR ; true}}
{{'AndR ; 'AndL ; true}}
{{'AndR ; 'AndR ; true}}
{{'AndR ; 'I ; true}}
{{'AndR ; 'ImpL ; true}}
{{'AndR ; 'ImpR ; true}}
{{'AndR ; 'OrL ; true}}
{{'AndR ; 'OrR1 ; true}}
{{'AndR ; 'OrR2 ; true}}
{{'AndR ; 'botL ; true}}
{{'AndR ; 'topL ; true}}
{{'AndR ; 'topR ; true}}
{{'I ; 'AndL ; true}}
{{'I ; 'AndR ; true}}
{{'I ; 'I ; true}}
{{'I ; 'ImpL ; true}}
{{'I ; 'ImpR ; true}}
{{'I ; 'OrL ; true}}
{{'I ; 'OrR1 ; true}}
{{'I ; 'OrR2 ; true}}
{{'I ; 'botL ; true}}
{{'I ; 'topL ; true}}
{{'I ; 'topR ; true}}
{{'ImpL ; 'AndL ; true}}
{{'ImpL ; 'AndR ; true}}
{{'ImpL ; 'I ; true}}
{{'ImpL ; 'ImpL ; true}}
{{'ImpL ; 'ImpR ; false}}
{{'ImpL ; 'OrL ; true}}
{{'ImpL ; 'OrR1 ; true}}
{{'ImpL ; 'OrR2 ; true}}
{{'ImpL ; 'botL ; true}}
{{'ImpL ; 'topL ; true}}
{{'ImpL ; 'topR ; true}}
{{'ImpR ; 'AndL ; true}}
{{'ImpR ; 'AndR ; true}}
{{'ImpR ; 'I ; true}}
{{'ImpR ; 'ImpL ; false}}
{{'ImpR ; 'ImpR ; true}}
{{'ImpR ; 'OrL ; true}}
{{'ImpR ; 'OrR1 ; true}}
{{'ImpR ; 'OrR2 ; true}}
{{'ImpR ; 'botL ; true}}
{{'ImpR ; 'topL ; true}}
{{'ImpR ; 'topR ; true}}
{{'OrL ; 'AndL ; true}}
{{'OrL ; 'AndR ; true}}
{{'OrL ; 'I ; true}}
{{'OrL ; 'ImpL ; true}}
{{'OrL ; 'ImpR ; true}}
{{'OrL ; 'OrL ; true}}
{{'OrL ; 'OrR1 ; false}}
{{'OrL ; 'OrR2 ; false}}
{{'OrL ; 'botL ; true}}
{{'OrL ; 'topL ; true}}
{{'OrL ; 'topR ; true}}
{{'OrR1 ; 'AndL ; true}}
{{'OrR1 ; 'AndR ; true}}
{{'OrR1 ; 'I ; true}}
{{'OrR1 ; 'ImpL ; true}}
{{'OrR1 ; 'ImpR ; true}}
{{'OrR1 ; 'OrL ; true}}
{{'OrR1 ; 'OrR1 ; true}}
{{'OrR1 ; 'OrR2 ; true}}
{{'OrR1 ; 'botL ; true}}
{{'OrR1 ; 'topL ; true}}
{{'OrR1 ; 'topR ; true}}
{{'OrR2 ; 'AndL ; true}}
{{'OrR2 ; 'AndR ; true}}
{{'OrR2 ; 'I ; true}}
{{'OrR2 ; 'ImpL ; true}}
{{'OrR2 ; 'ImpR ; true}}
{{'OrR2 ; 'OrL ; true}}
{{'OrR2 ; 'OrR1 ; true}}
{{'OrR2 ; 'OrR2 ; true}}
{{'OrR2 ; 'botL ; true}}
{{'OrR2 ; 'topL ; true}}
{{'OrR2 ; 'topR ; true}}
{{'botL ; 'AndL ; true}}
{{'botL ; 'AndR ; true}}
{{'botL ; 'I ; true}}
{{'botL ; 'ImpL ; true}}
{{'botL ; 'ImpR ; true}}
{{'botL ; 'OrL ; true}}
{{'botL ; 'OrR1 ; true}}
{{'botL ; 'OrR2 ; true}}
{{'botL ; 'botL ; true}}
{{'botL ; 'topL ; true}}
{{'botL ; 'topR ; true}}
{{'topL ; 'AndL ; true}}
{{'topL ; 'AndR ; true}}
{{'topL ; 'I ; true}}
{{'topL ; 'ImpL ; true}}
{{'topL ; 'ImpR ; true}}
{{'topL ; 'OrL ; true}}
{{'topL ; 'OrR1 ; true}}
{{'topL ; 'OrR2 ; true}}
{{'topL ; 'botL ; true}}
{{'topL ; 'topL ; true}}
{{'topL ; 'topR ; true}}
{{'topR ; 'AndL ; true}}
{{'topR ; 'AndR ; true}}
{{'topR ; 'I ; true}}
{{'topR ; 'ImpL ; true}}
{{'topR ; 'ImpR ; true}}
{{'topR ; 'OrL ; true}}
{{'topR ; 'OrR1 ; true}}
{{'topR ; 'OrR2 ; true}}
{{'topR ; 'botL ; true}}
{{'topR ; 'topL ; true}}
{{'topR ; 'topR ; true}}

In this output, the second rule permutes down the first one.

`System mLJ`

Now we turn our attention to the system mLJ (multi-conclusion intuitionistic propositional logic). The specification can be found in the file test_mlj.maude.

mod mLJ is
    pr SEQUENT .
    pr META-LEVEL .
    var P : Prop .
    vars F G H : Formula .
    var C C' : SFormula .
    ops ANY : -> SFormula .
    
    rl [I] : P ; C |- P ; C' => proved .
    rl [AndL] : F /\ G ; C |- C' => F ; G ; C |- C' .
    rl [AndR] : C |- F /\ G ; C' => (C |- F ; C') , (C |- G ; C') .
    rl [botL] : C ; False |- C' => proved .
    rl [topR] : C |- True ; C' => proved .
    rl [topL] : C ; True |- C' => C |- C' .
    rl [OrL] : C ; F \/ G |- C' => (C ; F |- C') , (C ; G |- C') .
    rl [OrR] : C |- F \/ G ; C' =>  C |- F ; G ; C' .
    rl [ImpR] : C |- (F --> G) ; C' =>  C ; F |- G .
    rl [ImpL] : C ; F --> G |- C' => (C ; F --> G |- F ; C') , (C ; G |- C') .
endm

In mLJ weakening and contraction are admissible rules. Moreover, all the rules are invertible but implication right. The prover is able to prove all these properties. As in the previous cases, the admissibility of contraction requires to assume all the already proved invertibility lemmas.

select THEOREM-PROVING-mLJ .
red invertibility . 
result Result: {'AndL ; true}
{'AndR ; true}
{'I ; true}
{'ImpL ; true}
{'ImpR ; false}
{'OrL ; true}
{'OrR ; true}
{'botL ; true}
{'topL ; true}
{'topR ; true}

red admissible?(Th-Imp) .
result Bool: true

red admissible?(Th-WeakeningL) .
result Bool: true

red admissible?(Th-WeakeningR) .
result Bool: true

`Classical Propositional Logic (System G3cp)`

The system G3cp for classical propositional logic is specified in the file test_g3cp.
In this case, all the rules are invertible and the prover succeeds to prove it, as well as the admissibility of Weakening:

select THEOREM-PROVING-G3c .
red invertibility .

result Result: {'AndL ; true}
{'AndR ; true}
{'I ; true}
{'ImpL ; true}
{'ImpR ; true}
{'OrL ; true}
{'OrR ; true}
{'botL ; true}
{'topL ; true}
{'topR ; true}


red admissible?(Th-Weakening) .
result Bool: true

Now that we have shown that all the rules are invertible, we can show the admissibility of Contraction:

select THEOREM-PROVING-G3cInv .
red admissible?(Th-Contraction) .
result Bool: true

Moreover, also assuming the already proved invertibility lemmas, we can show that all rules permute down:

select THEOREM-PROVING-G3cInv .
red analyzePermutation .
result Result: {{'AndL ; 'AndL ; true}}
{{'AndL ; 'AndR ; true}}
{{'AndL ; 'I ; true}}
{{'AndL ; 'ImpL ; true}}
{{'AndL ; 'ImpR ; true}}
{{'AndL ; 'OrL ; true}}
{{'AndL ; 'OrR ; true}}
{{'AndL ; 'botL ; true}}
{{'AndL ; 'topL ; true}}
{{'AndL ; 'topR ; true}}
{{'AndR ; 'AndL ; true}}
{{'AndR ; 'AndR ; true}}
{{'AndR ; 'I ; true}}
{{'AndR ; 'ImpL ; true}}
{{'AndR ; 'ImpR ; true}}
{{'AndR ; 'OrL ; true}}
{{'AndR ; 'OrR ; true}}
{{'AndR ; 'botL ; true}}
{{'AndR ; 'topL ; true}}
{{'AndR ; 'topR ; true}}
{{'I ; 'AndL ; true}}
{{'I ; 'AndR ; true}}
{{'I ; 'I ; true}}
{{'I ; 'ImpL ; true}}
{{'I ; 'ImpR ; true}}
{{'I ; 'OrL ; true}}
{{'I ; 'OrR ; true}}
{{'I ; 'botL ; true}}
{{'I ; 'topL ; true}}
{{'I ; 'topR ; true}}
{{'ImpL ; 'AndL ; true}}
{{'ImpL ; 'AndR ; true}}
{{'ImpL ; 'I ; true}}
{{'ImpL ; 'ImpL ; true}}
{{'ImpL ; 'ImpR ; true}}
{{'ImpL ; 'OrL ; true}}
{{'ImpL ; 'OrR ; true}}
{{'ImpL ; 'botL ; true}}
{{'ImpL ; 'topL ; true}}
{{'ImpL ; 'topR ; true}}
{{'ImpR ; 'AndL ; true}}
{{'ImpR ; 'AndR ; true}}
{{'ImpR ; 'I ; true}}
{{'ImpR ; 'ImpL ; true}}
{{'ImpR ; 'ImpR ; true}}
{{'ImpR ; 'OrL ; true}}
{{'ImpR ; 'OrR ; true}}
{{'ImpR ; 'botL ; true}}
{{'ImpR ; 'topL ; true}}
{{'ImpR ; 'topR ; true}}
{{'OrL ; 'AndL ; true}}
{{'OrL ; 'AndR ; true}}
{{'OrL ; 'I ; true}}
{{'OrL ; 'ImpL ; true}}
{{'OrL ; 'ImpR ; true}}
{{'OrL ; 'OrL ; true}}
{{'OrL ; 'OrR ; true}}
{{'OrL ; 'botL ; true}}
{{'OrL ; 'topL ; true}}
{{'OrL ; 'topR ; true}}
{{'OrR ; 'AndL ; true}}
{{'OrR ; 'AndR ; true}}
{{'OrR ; 'I ; true}}
{{'OrR ; 'ImpL ; true}}
{{'OrR ; 'ImpR ; true}}
{{'OrR ; 'OrL ; true}}
{{'OrR ; 'OrR ; true}}
{{'OrR ; 'botL ; true}}
{{'OrR ; 'topL ; true}}
{{'OrR ; 'topR ; true}}
{{'botL ; 'AndL ; true}}
{{'botL ; 'AndR ; true}}
{{'botL ; 'I ; true}}
{{'botL ; 'ImpL ; true}}
{{'botL ; 'ImpR ; true}}
{{'botL ; 'OrL ; true}}
{{'botL ; 'OrR ; true}}
{{'botL ; 'botL ; true}}
{{'botL ; 'topL ; true}}
{{'botL ; 'topR ; true}}
{{'topL ; 'AndL ; true}}
{{'topL ; 'AndR ; true}}
{{'topL ; 'I ; true}}
{{'topL ; 'ImpL ; true}}
{{'topL ; 'ImpR ; true}}
{{'topL ; 'OrL ; true}}
{{'topL ; 'OrR ; true}}
{{'topL ; 'botL ; true}}
{{'topL ; 'topL ; true}}
{{'topL ; 'topR ; true}}
{{'topR ; 'AndL ; true}}
{{'topR ; 'AndR ; true}}
{{'topR ; 'I ; true}}
{{'topR ; 'ImpL ; true}}
{{'topR ; 'ImpR ; true}}
{{'topR ; 'OrL ; true}}
{{'topR ; 'OrR ; true}}
{{'topR ; 'botL ; true}}
{{'topR ; 'topL ; true}}
{{'topR ; 'topR ; true}}

`Systems for Linear Logic`

We specify the monadic (file test_llM.maude) and the dyadic system (file test_llD.maude) for linear logic.

`Monadic System`

In this system the prover is able to successfully prove all the invertible rules:

red invertibility . 
result Result: {'bang ; false}
{'bot ; true}
{'init ; true}
{'one ; true}
{'par ; true}
{'plusA ; false}
{'plusB ; false}
{'quest ; false}
{'questC ; true}
{'questW ; false}
{'tensor ; false}
{'top ; true}
{'with ; true}

Moreover, the tool is able to prove that |- Gamma, ! F implies |- Gamma, F

red admissible?(Th-Bang) .
result Bool: true

`Dyadic System`

For the dyadic system, the result is as follows:

select THEOREM-PROVING-LL-DYADIC .
red invertibility .
result Result: {'bang ; false}
{'bot ; true}
{'copy ; false}
{'init ; true}
{'initC ; true}
{'initC ; true}
{'one ; true}
{'par ; true}
{'plusA ; false}
{'plusB ; false}
{'quest ; false}
{'tensor ; false}
{'top ; true}
{'with ; true}

In this system, the rule ? (quest in the output) is invertible. However, the system is not able to prove it. The reason is that such proof requires an additional lemma: the admissibility of weakening in the classical context that we proved as follows:

--- Specification of the theorem 
    op Th-WeakeningC : -> Rule .
    eq Th-WeakeningC = ( rl '|-`[_`]_['CC:SFormula,'CL:MSFormula] => '|-`[_`]_['_;_['ANY.SFormula,'CC:SFormula],'CL:MSFormula] [ label('Th-Weakening) ]. ) .

--- Result
red admissible?(Th-WeakeningC) .
result Bool: true

The system LL-DYADIC-W (dyadic system + weakening on the classical context) is able to prove the invertibility of ?:

select THEOREM-PROVING-LL-DYADIC-W .
red invertibility .
result Result: {'W ; false}
{'bang ; false}
{'bot ; true}
{'copy ; false}
{'init ; true}
{'initC ; true}
{'initC ; true}
{'one ; true}
{'par ; true}
{'plusA ; false}
{'plusB ; false}
{'quest ; true}
{'tensor ; false}
{'top ; true}
{'with ; true}

As in the previous examples, the permutability of rules require the invertibility lemmas already proved.

select THEOREM-PROVING-LL-DYADIC-INV .
red analyzePermutation .

`Modal Logics: K and S4`

In file test_modalK.maude we specified sequent systems for the modal logics K and S4.

`K`

In the logic K, all the propositional rules are invertible and the modal rule K is not. The discussion about admissibility of weakening and contraction follows similarly to the previous examples.

select  THEOREM-PROVING-K .
red invertibility .
result Result: {'I ; true}
{'K ; false}
{'botL ; true}
{'botR ; true}
{'conjL ; true}
{'conjR ; true}
{'disjL ; true}
{'disjR ; true}
{'impL ; true}
{'impR ; true}
{'topL ; true}
{'topR ; true}

red admissible?(Th-Weakening) .
result Bool: true

--- Assuming the previous lemmas about invertibility, we prove contraction to be admissible
select THEOREM-PROVING-K-CONTRACTION .
red admissible?(Th-Contraction) .
result Bool: true

`S4`

In the system S4, all the propositional rules are invertible as well as the modal rule T. The prover is able to show all these properties.

select  THEOREM-PROVING-S4 .
red invertibility .
result Result: {'4 ; false}
{'I ; true}
{'K ; false}
{'T ; true}
{'botL ; true}
{'botR ; true}
{'conjL ; true}
{'conjR ; true}
{'disjL ; true}
{'disjR ; true}
{'impL ; true}
{'impR ; true}
{'topL ; true}
{'topR ; true}

red admissible?(Th-Weakening) .
result Bool: true

--- Assuming the previous lemmas about invertibility, we prove contraction to be admissible
select THEOREM-PROVING-S4-CONTRACTION .
red admissible?(Th-Contraction) .
result Bool: true