Material 2

%%%
% 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)
]
).

Comments