%%% Cut-Free Intuitionistic Sequent Calculus
%%% Propositional Logic
%%% Tabling achieves loop-detection based sequent calculus
%%% Interesting question: can we model Howe's loop detection mechanism?

%%% Author: Frank Pfenning

hyp  : o -> type.  % Hypotheses (left)
conc : o -> type.  % Conclusion (right)
%name hyp H.
%name conc D.
%tabled hyp.
%tabled conc.

impr  : conc (A imp B)
	 <- (hyp A -> conc B).

impl  : (hyp (A imp B) -> conc C)
	 <- conc A
	 <- (hyp B -> conc C).

andr  : conc (A and B)
	 <- conc A
	 <- conc B.

andl1 : (hyp (A and B) -> conc C)
	 <- (hyp A -> conc C).


andl2 : (hyp (A and B) -> conc C)
	 <- (hyp B -> conc C).

orr1  : conc A
	 -> conc (A or B).

orr2  : conc B
	 -> conc (A or B).

orl   : (hyp A -> conc C)
	 -> (hyp B -> conc C)
	 -> (hyp (A or B) -> conc C).


notr  : ({p:o} hyp A -> conc p)
	 -> conc (not A).

notl  : conc A
	 -> (hyp (not A) -> conc C).

axiom : (hyp (atom P) -> conc (atom P)).

truer : conc (true).

falsel : (hyp (false) -> conc C).