seq_cal.pl

axiom([A | _], [A | _]).

andLL([and(A, _) | Gamma], Delta) :- solve([A | Gamma], Delta).
andLR([and(_, B) | Gamma], Delta) :- solve([B | Gamma], Delta).
andI(Gamma, [and(A, B)]) :-
    solve(Gamma, [A]),
    solve(Gamma, [B]).

orLL(Gamma, [or(A, _) | Delta]) :- solve(Gamma, [A | Delta]).
orLR(Gamma, [or(_, B) | Delta]) :- solve(Gamma, [B | Delta]).
orI([or(A, B) | Gamma], Delta) :-
    solve([A | Gamma], Delta),
    solve([B | Gamma], Delta).

notL(Gamma, [neg(A) | Delta]) :- solve([A | Gamma], Delta).
notR([neg(B) | Gamma], Delta) :- solve(Gamma, [B | Delta]).

implL([impl(A, B) | Left], Delta) :-
    append(Gamma, Pi, Left),
    solve(Gamma, [ A ]),
    solve([B | Pi], Delta).
implR(Gamma, [impl(A, B) | Delta]) :- solve([A | Gamma], [B | Delta]).

solve_(Gamma, Delta) :- axiom(Gamma, Delta).
solve_(Gamma, Delta) :- andLL(Gamma, Delta).
solve_(Gamma, Delta) :- andLR(Gamma, Delta).
solve_(Gamma, Delta) :- andI(Gamma, Delta).
solve_(Gamma, Delta) :- orLL(Gamma, Delta).
solve_(Gamma, Delta) :- orLR(Gamma, Delta).
solve_(Gamma, Delta) :- orI(Gamma, Delta).
solve_(Gamma, Delta) :- notL(Gamma, Delta).
solve_(Gamma, Delta) :- notR(Gamma, Delta).
solve_(Gamma, Delta) :- implL(Gamma, Delta).
solve_(Gamma, Delta) :- implR(Gamma, Delta).

solve_([_ | Gamma], Delta) :- solve(Gamma, Delta). % Weakening
solve_(Gamma, [_ | Delta]) :- solve(Gamma, Delta). % Weakening
solve(Gamma, Delta) :- solve(Gamma, Delta, 0, 0).
solve(Gamma, Delta, _, _) :-                             % Exchange
    permutation(Gamma, Gamma_),
    permutation(Delta, Delta_),
    solve_(Gamma_, Delta_).