---------------------------------------------
*** Knotted Systems (2-3 Rule)
---------------------------------------------
--- This file implements the system FLEW_2 which is FLEW + 2-3 Rule (Figure 2 in [1]).
--- No lazy strategy is implemented in this case.
--- The problem with implication in the classical context disappear thanks to the search strategy of Maude: loops are automatically detected since the set of sequents to be proved is idempotent.
--- Invertible rules are implemented as part of the equational theory. The non-invertible ones as (conditional) rules in the Module.
--- Sequents has the shape [CC] LC ==> G where CC is the classical context, LC the linear context and G the goal.
--- Some examples of use are in the end of the file.
--- @author Carlos Olarte
---------------------------------------------
set include BOOL on .
fmod KN-SIG is
sorts
Prop *** propositions
Formula *** formulas
Context *** Set --classical-- or multiset --linear-- of formulas.
Sequent . *** Sequent
sort SSequent . *** Sets of sequents
subsort Prop < Formula < Context .
subsort Sequent < SSequent .
*** Sequent definitions
op [_]_==>_ : Context Context Formula -> Sequent [ctor format (bu s s o osur d o)] .
op proved : -> Sequent [format (g! o)] .
op failed : -> Sequent .
*** Context definitions
op - : -> Context [ctor] . *** empty
op _,_ : Context Context -> Context [ctor assoc comm prec 60 id: -] .
*** sets of sequents
op _|_ : SSequent SSequent -> SSequent [ctor assoc comm prec 80] .
var A1 A2 A3 : Prop . *** Atoms
var F G H : Formula .
var CC Ca Cb : Context .
var LC : Context .
var Sq : Sequent .
var SS : SSequent .
*** Structural rules
eq [CC,F,F] LC ==> G = [CC,F] LC ==> G . *** Idempotency on the classical context (set representation)
eq [CC] LC,F,F ==> G = [CC,F] LC ==> G . *** Knotted rule: 2 linear copies become classical
eq [CC, F] LC, F ==> G = [CC,F] LC ==> G . *** Linear copies simplify with classical copies
*** Structural rules for sets of sequents
*** idempotency (e.g., 2 equal sequents become one. it also avoids loops due to the impl. on the classical context
eq Sq | Sq = Sq .
eq Sq | proved = Sq .
eq Sq | failed = failed .
*** Formulas
op top : -> Formula [ctor] .
op bot : -> Formula [ctor] .
op one : -> Formula [ctor] .
ops p q r s t a b c d e f g h : -> Prop .
op _*_ : Formula Formula -> Formula [ctor comm assoc prec 30] . *** multiplicative conjunction (otimes)
op _-*_ : Formula Formula -> Formula [ctor prec 40 gather (e E)] .
op _+_ : Formula Formula -> Formula [ctor comm assoc prec 35] . *** disjunction
op _&_ : Formula Formula -> Formula [ctor comm assoc prec 35] . *** additive conjunction
*** Invertiable rules as equations
eq [CC, A1] LC ==> A1 = proved . *** Initial with weakining (classical case)
eq [CC] LC, A1 ==> A1 = proved . *** Initial with weakining (linear case)
eq [CC] LC, (F * G) ==> H = [CC] LC, F, G ==> H . *** multiplicative conjunction
eq [CC, F * G] LC ==> H = [CC, F, G] LC ==> H . *** multiplicative conjunction
eq [CC] LC ==> top = proved . *** Top on the right + weakening
eq [CC, bot] LC ==> G = proved . *** bottom on the right (classical case)
eq [CC] LC, bot ==> G = proved . *** bottom on the right (multiplicative case)
eq [CC] LC ==> F -* G = [CC] LC, F ==> G . *** implication right
eq [CC, one] LC ==> G = [CC] LC ==> G . *** weakening of one
eq [CC] LC, one ==> G = [CC] LC ==> G . *** weakening of one
eq [CC] LC ==> one = proved . *** one + weakening
eq [CC] LC, F + G ==> H = ( [CC] LC, F ==> H ) | ( [CC] LC, G ==> H ) . *** disjunction (linear case)
eq [CC, F + G] LC ==> H = ( [CC, F] LC ==> H ) | ( [CC, G] LC ==> H ) . *** disjunction (classical case)
eq [CC, F & G] LC ==> H = [CC, F, G] LC ==> H . *** Additive conjunction in the classical context becomes tensor
eq [CC] LC ==> F & G = ( [CC] LC ==> F ) | [CC] LC ==> G . *** Additive conjunction on the right
*** Rules LCC and LCG: Avoid loops due to implications in the classical context
eq [CC, F, F -* G] LC ==> H = [CC, G] LC ==> H .
eq [CC, G, F -* G] LC ==> H = [CC, G] LC ==> H .
*** Some functions on contexts
*** Check if bot appears (possitively) in a formula
op hasBot : Formula -> Bool .
eq hasBot(bot) = true .
eq hasBot(top) = false .
eq hasBot(one) = false .
eq hasBot(A1) = false .
eq hasBot(F * G) = hasBot(F) or hasBot(G) .
eq hasBot(F + G) = hasBot(F) or hasBot(G) .
eq hasBot(F -* G) = hasBot(G) . *** F is not checked (only positive occurrences)
eq hasBot(F & G) = hasBot(F) or hasBot(G) .
op hasBot : Context -> Bool .
eq hasBot(-) = false .
eq hasBot(F, Ca) = hasBot(F) or hasBot(Ca) .
*** Check if an atom occurs (possitively) in a formula
op hasAtom : Prop Formula -> Bool .
eq hasAtom(A1, bot) = false .
eq hasAtom(A1, top) = false .
eq hasAtom(A1, one) = false .
eq hasAtom(A1, A1) = true .
ceq hasAtom(A1, A2) = false if A1 =/= A2 .
eq hasAtom(A1, F * G) = hasAtom(A1, F) or hasAtom(A1, G) .
eq hasAtom(A1, F + G) = hasAtom(A1, F) or hasAtom(A1, G) .
eq hasAtom(A1, F -* G) = hasAtom(A1, G) .
eq hasAtom(A1, F & G) = hasAtom(A1, F) or hasAtom(A1, G) .
op hasAtom : Prop Context -> Bool .
eq hasAtom(A1, -) = false .
eq hasAtom(A1, (F, Ca)) = hasAtom(A1, F) or hasAtom(A1, Ca) .
*** Failing axioms
ceq [CC] LC ==> A1 = failed if hasBot((CC, LC)) == false and hasAtom(A1, (CC, LC)) == false .
ceq [CC] LC ==> A1 * F = failed if hasBot((CC, LC)) == false and hasAtom(A1, (CC, LC)) == false .
endfm
mod KN is
including KN-SIG .
var CC : Context .
var SS : SSequent .
var CtA CtB CtC CtD : Context .
var LC Delta Delta1 Delta2 : Context .
var F G H : Formula .
*** Conjunction right (without lazy splitting)
rl [conj-R] : ([CC] CtA, CtB ==> F * G) => ([CC] CtB ==> G) | ([CC] CtA ==> F) .
*** Implication on the linear context
rl [impl-LL] : ([CC] CtA, CtB, F -* G ==> H) => ([CC] CtA ==> F) | ([CC] CtB, G ==> H) .
*** Implication in the classical context
rl [impl-LC] : ([CC, F -* G] CtA, CtB ==> H) => ( [CC, F -* G] CtA ==> F ) | ([CC, F -* G] CtB, G ==> H) .
*** Aditivie conjunction (In the classical context F&G == F * G and the rule is handled in the equational theort)
rl [conj-LL] : ([CC] Delta, F & G ==> H ) => [CC] Delta, F ==> H .
rl [disj-LR] : ([CC] Delta, F & G ==> H ) => [CC] Delta, G ==> H .
*** Disjunction
rl [disj-RL] : ([CC] Delta ==> F + G) => ([CC] Delta ==> F) .
rl [disj-RR] : ([CC] Delta ==> F + G) => ([CC] Delta ==> G) .
*** Knotted rule
crl [kn-32] : ([CC] Delta, Delta1, Delta2 ==> F) => ([CC, Delta1] Delta ==> F) | [CC, Delta2] Delta ==> F if Delta1 =/= - /\ Delta2 =/= - .
endm
*****************
*** End of Module
*****************
*****************
*** SOME TEST
*****************
***(
*** proofs using knotted rule (25ms)
search [1] [-] r, r -* p -* q, p -* q, (p -* q) -* (p -* q) -* (p -* q) -* s ==> s =>* proved .
*** The example of the paper (2ms)
search [1] [-] p -* bot, p -* q ==> (p -* q) * (p -* q) * (p -* q) =>* proved .
*** the couterexample for cut-elimination (simplified) 51 ms
search [1] [-] r, p -* r -* q, p -* q ==> (p -* q) * (p -* q) * (p -* q) =>* proved .
*** the couterexample for cut-elimination. (84 ms)
search [1] [-] r, p -* r -* q, p -* q, (p -* q) * (p -* q) * (p -* q) -* s ==> s =>* proved .
*** the couterexample for cut-elimination. (171 ms)
search [1] [-] r, p -* r -* q, p -* q, (p -* q) -* ( (p -* q) -* ( (p -* q) -* s ) ) ==> s =>* proved .
*** Disjunction (160 ms)
search [1] [-] a, b, c, d ==> (a * c * c * a) + (b * d * d * b) =>* proved .
*** an example that needs twice an implication (in the classical context) (0ms)
search [1] [-] p -* q, p -* q, p, (p -* q) -* q ==> q * q =>* proved .
*** same example for cut-elim but with "trash" formulas in the context ... never ending (for the moment).
search [1] [-] s -* s, r, p -* r -* q, p -* q, (p -* q) * (p -* q) * (p -* q) -* s ==> s =>* proved .
) *** end of the comment