% Background theory about natural numbers and booleans nat : type. %name nat X. z : nat. s : nat -> nat. bool: type. %name bool B. true: bool. false: bool. % Horn Theory for even/odd even: nat -> type. %name even P. odd: nat -> type. %name odd F. e_z: even z. o_s: odd (s X) <- even X. e_s: even (s X) <- odd X. %query 1 4 D : even (s (s z)). % Horn Theory for plus plus : nat -> nat -> nat -> type. %name plus P. p_z : plus z Y Y. p_s : plus (s X) Y (s Z) <- plus X Y Z. % Derive Horn goal from Horn theory %query 1 4 D : plus (s z) z (s z). % Horn Theory for subtraction sub: nat -> nat -> nat -> type. %name sub S. s_z1 : sub X z X. s_z2 : sub z Y z. s_ss : sub (s X) (s Y) Z <- sub X Y Z. % Horn Theory for less less: nat -> nat -> bool -> type. %name less L. l_z1 : less z (s X) true. l_z2 : less X z false. l_ss : less (s X) (s Y) B <- less X Y B. % Horn Theory for greatest common divider gcd: nat -> nat -> nat -> type. %name gcd G. gcd_z1: gcd z Y Y. gcd_z2: gcd X z X. gcd_s1: gcd (s X) (s Y) Z <- less (s X) (s Y) true <- sub Y X Y' <- gcd (s X) Y' Z. gcd_s1: gcd (s X) (s Y) Z <- less (s X)(s Y) false <- sub X Y X' <- gcd X' (s Y) Z. % Horn Theory for Ackerman Function acker : nat -> nat -> nat -> type. a_1 : acker z Y (s Y). a_2 : acker (s X) z Z <- acker X (s z) Z. a_3 : acker (s X) (s Y) Z <- acker (s X) Y Z' <- acker X Z' Z.