% $Id: prf.pl,v 1.2 2024/08/28 11:43:15 oc45ujef Exp $
%!  prf(Proof, Context, Formula) is semidet.
%
%   A proof checker for propositional natural deduction in sequent
%   style.

prf(ctx, Gamma, X) :-
    memberchk(X, Gamma).        % [0]

prf(andEl(P), Gamma, X) :-
    prf(P, Gamma, X * _).

prf(andEr(P), Gamma, Y) :-
    prf(P, Gamma, _ * Y).

prf(andI(P, Q), Gamma, X * Y) :-
    prf(P, Gamma, X),
    prf(Q, Gamma, Y).

prf(orIl(P), Gamma, X + _) :-
    prf(P, Gamma, X).

prf(orIr(P), Gamma, _ + Y) :-
    prf(P, Gamma, Y).

prf(orE(P, Q, R), Gamma, Z) :-
    prf(P, Gamma, X + Y),
    prf(Q, [X | Gamma], Z),
    prf(R, [Y | Gamma], Z).

prf(impE(P, Q), Gamma, Y) :-
    prf(P, Gamma, X => Y),
    prf(Q, Gamma, X).

prf(impI(P), Gamma, X => Y) :-
    prf(P, [X | Gamma], Y).

prf(negI(P, Q), Gamma, ~(X)) :-
    prf(P, [X | Gamma], Y),
    prf(Q, [X | Gamma], ~(Y)).

prf(botI(P, Q), Gamma, bot) :-
    prf(P, Gamma, ~(X)),
    prf(Q, Gamma, X).

prf(botE(P), Gamma, _) :-
    prf(P, Gamma, bot).

prf(tnd, _, X + ~(X)).

% Examples ========================

% ----------- (tnd)
% ⊢ (A ∨ ¬ A)
%
% ?- prf(tnd, [], a + ~(a)).

%    ----- (ctx)
%    ⊥ ⊢ ⊥
% ------------- (botE)
% ⊥ ⊢ (A ∧ ¬ A)
%
% ?- prf(botE(ctx), [bot], (a + ~(a))).

%  ----------------- (ctx)     ------------------- (ctx)
%  (A ∧ B) ⊢ (A ∧ B)            (A ∧ B) ⊢ (A ∧ B)
%  ----------------- (andEl)   ------------------- (andEr)
%     (A ∧ B) ⊢ A                (A ∧ B) ⊢ B
% ------------------------------------------------ (andI)
%                   (A ∧ B) ⊢ (B ∧ A)
% ------------------------------------------------ (impI)
%                 ⊢ (A ∧ B) ⇒ (B ∧ A)
%
% ?- prf(impI(andI(andEr(ctx), andEl(ctx))), [], (a * b) => (b * a)).

% Footnotes =======================
% [0] Note the use of `memberchk/2` instead of `member/2`.  The former
%     is semi-deterministic (i.e. it succeeds at most once), while the
%     latter is not.