%%% Cut-Free Intuitionistic Sequent Calculus
%%% 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 A -> conc A).

truer : conc (true).

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

%{
forallr : ({a:i} conc (A a))
	   -> conc (forall A). 

foralll : {T:i} (hyp (A T) -> conc C)
	   -> (hyp (forall A) -> conc C).

existsr : {T:i} conc (A T)
	   -> conc (exists A).

existsl : ({a:i} hyp (A a) -> conc C)
	   -> (hyp (exists A) -> conc C).

}%