% The following is a near direct specification of the proof system
% of Forum (given in TCS draft, Figure 1)

% The right predicate encodes the sequent used to do
% right-introductions.
% The left predicate encodes the sequent used to do
% left-introductions (backchaining).

module one.
import forumlog aux.

type right    list o -> list o -> list o -> list o -> list o -> o.
type left     list o -> list o -> o -> list o -> list o -> o.

right Psi Delta Atoms nil Upsilon :-
  membNrest B Delta Rest, left  Psi Rest  B Atoms Upsilon;
  memb      B Psi,        left  Psi Delta B Atoms Upsilon;
  memb      B Upsilon,    right Psi Delta Atoms (B::nil) Upsilon.

right Psi Delta Atoms (Atom::Gamma) Upsilon :-
  atomic Atom, right Psi Delta (Atom::Atoms) Gamma Upsilon.

right Psi Delta Atoms (erase::Gamma) Upsilon.

right Psi Delta Atoms ((B & C)::Gamma) Upsilon :-
  right Psi Delta Atoms (B::Gamma) Upsilon,
  right Psi Delta Atoms (C::Gamma) Upsilon.

right Psi Delta Atoms (bottom::Gamma) Upsilon :-
  right Psi Delta Atoms Gamma Upsilon.

right Psi Delta Atoms ((B | C)::Gamma) Upsilon :-
  right Psi Delta Atoms (B::C::Gamma) Upsilon.

right Psi Delta Atoms ((B -o C)::Gamma) Upsilon :-
  right Psi (B::Delta) Atoms (C::Gamma) Upsilon.

right Psi Delta Atoms ((C o- B)::Gamma) Upsilon :-
  right Psi (B::Delta) Atoms (C::Gamma) Upsilon.

right Psi Delta Atoms ((B => C)::Gamma) Upsilon :-
  right (B::Psi) Delta Atoms (C::Gamma) Upsilon.

right Psi Delta Atoms ((pi B)::Gamma) Upsilon :-
  pi x\(right Psi Delta Atoms ((B x)::Gamma) Upsilon).

right Psi Delta Atoms ((? B)::Gamma) Upsilon :-
  right Psi Delta Atoms Gamma (B::Upsilon).

left Psi nil A (A::nil) Upsilon.

left Psi nil A nil Upsilon :- memb A Upsilon.

left Psi nil bottom nil Psi.

left Psi Delta (B & C) Atoms Upsilon :- 
  left Psi Delta B Atoms Upsilon; left Psi Delta C Atoms Upsilon.

left Psi nil (? B) nil Upsilon :- right Psi (B::nil) nil nil Upsilon.

left Psi Delta (B | C) Atoms Upsilon :-
  split Delta Delta1 Delta2, split Atoms Atoms1 Atoms2,
  left Psi Delta1 B Atoms1 Upsilon,
  left Psi Delta2 C Atoms2 Upsilon.

left Psi Delta (pi B) Atoms Upsilon :- left Psi Delta (B T) Atoms Upsilon.

left Psi Delta (B -o C) Atoms Upsilon :-
  split Delta Delta1 Delta2, split Atoms Atoms1 Atoms2,
  right Psi Delta1 Atoms1 (B::nil) Upsilon,
  left  Psi Delta2 C Atoms2 Upsilon.

left Psi Delta (C o- B) Atoms Upsilon :-
  split Delta Delta1 Delta2, split Atoms Atoms1 Atoms2,
  right Psi Delta1 Atoms1 (B::nil) Upsilon,
  left  Psi Delta2 C Atoms2 Upsilon.

left Psi Delta (B => C) Atoms Upsilon :-
  right Psi nil nil (B::nil) Upsilon,
  left  Psi Delta C Atoms Upsilon.