%%% % Date: 2012/07/23 % Made by Yoshitaka Yamamoto % Reference: Heuristic Inverse Subsumption in Full-clausal Theories %%% %%% Mode declaration %%% modeh(1, plus(+num, +num, -num)). modeb(1, plus(-num, -num, -num)). modeb(3, suc(-num, -num)). % Target hypothesis % plus(X, Y, Z) :- plus(X, V, U), suc(V, Y), suc(U, Z) % The above corresponds to the equation X + Y = Z if X + (Y - 1) = Z - 1. % Note that the predicate suc(V, Y) means Y = V + 1. % Note that the bridge theory F is set as B and -E in the experiment. %%% Type %%% type(0, num). type(1, num). type(2, num). type(3, num). type(4, num). type(5, num). %%% 10 Positive examples %%% cnf(an, obs, [plus(1, 1, 2)]). cnf(an, obs, [plus(1, 2, 3)]). cnf(an, obs, [plus(2, 1, 3)]). cnf(an, obs, [plus(1, 3, 4)]). cnf(an, obs, [plus(3, 1, 4)]). cnf(an, obs, [plus(1, 4, 5)]). cnf(an, obs, [plus(4, 1, 5)]). cnf(an, obs, [plus(2, 2, 4)]). cnf(an, obs, [plus(2, 3, 5)]). cnf(an, obs, [plus(3, 2, 5)]). %%% Background theory %%% cnf(an, bg, [suc(0, 1)]). cnf(an, bg, [suc(1, 2)]). cnf(an, bg, [suc(2, 3)]). cnf(an, bg, [suc(3, 4)]). cnf(an, bg, [suc(4, 5)]). cnf(an, bg, [plus(0, 0, 0)]). cnf(an, bg, [plus(0, 1, 1)]). cnf(an, bg, [plus(0, 2, 2)]). cnf(an, bg, [plus(0, 3, 3)]). cnf(an, bg, [plus(0, 4, 4)]). cnf(an, bg, [plus(0, 5, 5)]). cnf(an, bg, [plus(1, 0, 1)]). cnf(an, bg, [plus(2, 0, 2)]). cnf(an, bg, [plus(3, 0, 3)]). cnf(an, bg, [plus(4, 0, 4)]). cnf(an, bg, [plus(5, 0, 5)]). %%% Induction field %%% induction_field( length[0:], size[0:] ,[ +-plus(1, 1, 2), +-plus(1, 2, 3), +-plus(2, 1, 3), +-plus(1, 3, 4), +-plus(3, 1, 4), +-plus(1, 4, 5), +-plus(4, 1, 5), +-plus(2, 2, 4), +-plus(2, 3, 5), +-plus(3, 2, 5), -plus(0, 0, 0), -plus(0, 1, 1), -plus(0, 2, 2), -plus(0, 3, 3), -plus(0, 4, 4), -plus(0, 5, 5), -plus(1, 0, 1), -plus(2, 0, 2), -plus(3, 0, 3), -plus(4, 0, 4), -plus(5, 0, 5), -suc(0, 1), -suc(1, 2), -suc(2, 3), -suc(3, 4), -suc(4, 5), -suc(5, 6), -suc(6, 7), -suc(7, 8), -suc(8, 9) ] ). |
 | |
|
|