%
% NAL-Examples.txt
% Pei Wang 
% [All Rights Reserved]
% August 2004  
% Examples for NAL rules in the NAL Prolog program
% Each of the examples consists of a goal, followed by one or more expected results 
% (among the possible multiple results). To run it, copy the first line, then paste
% it into a Prolog interpreter.
%


% ----- NAL-1 ----- %

%% revision

revision([inheritance(bird, swimmer), [1, 0.8]], [inheritance(bird, swimmer), [0, 0.5]], R).
R = [inheritance(bird, swimmer), [0.8, 0.833333]] 


%% choice

choice([inheritance(swan, bird), [1, 0.8]], [inheritance(swan, bird), [0, 0.5]], R).
R = [inheritance(swan, bird), [1, 0.8]] ;

choice([inheritance(swan, bird), [1, 0.5]], [inheritance(penguin, bird), [0.8, 0.9]], R).
R = [inheritance(penguin, bird), [0.8, 0.9]] 


%% deduction

inference([inheritance(bird, animal), [1, 0.8]], [inheritance(robin, bird), [1, 0.8]], R).
R = [inheritance(robin, animal), [1, 0.64]]


%% induction

inference([inheritance(swan, swimmer), [1, 0.9]], [inheritance(swan, bird), [1, 0.9]], R).
R = [inheritance(bird, swimmer), [1, 0.390244]]


%% abduction

inference([inheritance(sport, competition), [1, 0.8]], [inheritance(chess, competition), [1, 0.8]], R).
R = [inheritance(chess, sport), [1, 0.390244]] 


%% examplification

inference([inheritance(robin, bird), [1, 0.8]], [inheritance(bird, animal), [1, 0.8]], R).
R = [inheritance(animal, robin), [1, 0.390244]]


%% convension

inference([inheritance(swan, bird), [0.9, 0.8]], R).
R = [inheritance(bird, swan), [1, 0.418605]] ;


% ----- NAL-2 ----- %


%% revision

revision([similarity(swan, robin), [1, 0.8]], [similarity(swan, robin), [0, 0.5]], R).
R = [similarity(swan, robin), [0.8, 0.833333]] 


%% merge

inference([inheritance(swan, bird), [1, 0.8]], [inheritance(bird, swan), [0.1, 0.8]], R).
R = [similarity(swan, bird), [0.1, 0.8992]]


%% comparison

inference([inheritance(swan, swimmer), [1, 0.8]], [inheritance(swan, bird), [1, 0.8]], R).
R = [similarity(bird, swimmer), [1, 0.390244]]

inference([inheritance(sport, competition), [1, 0.8]], [inheritance(chess, competition), [1, 0.8]], R).
R = [similarity(chess, sport), [1, 0.390244]] 


%% analogy

inference([inheritance(swan, swimmer), [1, 0.8]], [similarity(gull, swan), [1, 0.8]], R).
R = [inheritance(gull, swimmer), [1, 0.512]] ;

inference([inheritance(chess, competition), [1, 0.8]], [similarity(sport, competition), [1, 0.8]], R).
R = [inheritance(chess, sport), [1, 0.512]] 


%% deduction

inference([similarity(swan, robin), [1, 0.8]], [similarity(gull, swan), [1, 0.8]], R).
R = [similarity(gull, robin), [1, 0.64]]


%% convension --- the current version contains a bug to be fixed

inference([similarity(swan, bird), [0.9, 0.8]], [inheritance(swan, bird), V]).
V = [0.9, 0.72] ;

inference([inheritance(swan, bird), [0.9, 0.8]], [similarity(swan, bird), V]).
V = [0.9, 0.444444] ;

inference([inheritance(swan, bird), [1, 0.8]], [inheritance(bird, swan), [0.1, 0.8]], R).
R = [similarity(swan, bird), [0.1, 0.8992]] ;


%% instance and property

inference([instance(tweety, bird), [1, 0.8]], R).
R = [inheritance(ext_set([tweety]), bird), [1, 0.8]] 

inference([property(raven, black), [1, 0.8]], R).
R = [inheritance(raven, int_set([black])), [1, 0.8]]

inference([inst_prop(tweety, yellow), [1, 0.8]], R).
R = [inheritance(ext_set([tweety]), int_set([yellow])), [1, 0.8]] 


%% set definition

inference([inheritance(ext_set([tweety]), ext_set([birdie])), [1, 0.8]], R).
R = [similarity(ext_set([tweety]), ext_set([birdie])), [1, 0.8]]

inference([inheritance(int_set([smart]), int_set([bright])), [1, 0.8]], R).
R = [similarity(int_set([smart]), int_set([bright])), [1, 0.8]] 


%% structure transformation

inference([similarity(ext_set([tweety]), ext_set([birdie])), [1, 0.8]], R).
R = [similarity(tweety, birdie), [1, 0.8]]

inference([similarity(int_set([smart]), int_set([bright])), [1, 0.8]], R).
R = [similarity(smart, bright), [1, 0.8]]


% ----- NAL-3 ----- %

%% compound construction, two premises

inference([inheritance(swan, swimmer), [0.9, 0.9]], [inheritance(swan, bird), [0.8, 0.9]], R).
R = [inheritance(swan, ext_intersection([swimmer, bird])), [0.72, 0.858222]] ;
R = [inheritance(swan, int_intersection([swimmer, bird])), [0.98, 0.989892]] ;
R = [inheritance(swan, ext_difference(swimmer, bird)), [0.18, 0.951588]] ;

inference([inheritance(sport, competition), [0.9, 0.9]], [inheritance(chess, competition), [0.8, 0.9]], R).
R = [inheritance(int_intersection([sport, chess]), competition), [0.72, 0.858222]] ;
R = [inheritance(ext_intersection([sport, chess]), competition), [0.98, 0.989892]] ;
R = [inheritance(int_difference(sport, chess), competition), [0.18, 0.951588]] ;


%% compound construction, single premise

inference([inheritance(swan, swimmer), [0.9, 0.8]], [inheritance(swan, ext_intersection([swimmer, bird])), V]).
V = [0.9, 0.444444]

inference([inheritance(swan, swimmer), [0.9, 0.8]], [inheritance(swan, int_intersection([swimmer, bird])), V]).
V = [0.9, 0.72]

inference([inheritance(swan, swimmer), [0.9, 0.8]], [inheritance(swan, ext_difference(swimmer, bird)), V]).
V = [0.9, 0.444444] 

inference([inheritance(swan, swimmer), [0.9, 0.8]], [negation(inheritance(swan, ext_difference(bird, swimmer))), V]).
V = [0.9, 0.72] 

inference([inheritance(sport, competition), [0.9, 0.8]], [inheritance(int_intersection([sport, chess]), competition), V]).
V = [0.9, 0.444444] 

inference([inheritance(sport, competition), [0.9, 0.8]], [inheritance(ext_intersection([sport, chess]), competition), V]).
V = [0.9, 0.72]

inference([inheritance(sport, competition), [0.9, 0.8]], [inheritance(int_difference(sport, chess), competition), V]).
V = [0.9, 0.444444] 

inference([inheritance(sport, competition), [0.9, 0.8]], [negation(inheritance(int_difference(chess, sport), competition)), V]).
V = [0.9, 0.72] 


%% compound destruction, two premises

inference([inheritance(swan, bird), [1, 0.8]], [inheritance(swan, ext_intersection([swimmer, bird])), [0, 0.8]], R).
R = [inheritance(swan, swimmer), [0, 0.64]] ;

inference([inheritance(swan, bird), [0, 0.8]], [inheritance(swan, int_intersection([swimmer, bird])), [1, 0.8]], R).
R = [inheritance(swan, swimmer), [1, 0.64]] ;

inference([inheritance(swan, swimmer), [1, 0.8]], [inheritance(swan, ext_difference(swimmer, bird)), [0, 0.8]], R).
R = [inheritance(swan, bird), [1, 0.64]] ;

inference([inheritance(swan, bird), [0, 0.8]], [inheritance(swan, ext_difference(swimmer, bird)), [0, 0.8]], R).
R = [inheritance(swan, swimmer), [0, 0.64]] ;

inference([inheritance(sport, competition), [1, 0.8]], [inheritance(int_intersection([sport, chess]), competition), [0, 0.8]], [inheritance(chess, competition), V]).
V = [0, 0.64] 

inference([inheritance(sport, competition), [0, 0.8]], [inheritance(ext_intersection([sport, chess]), competition), [1, 0.8]], [inheritance(chess, competition), V]). 
V = [1, 0.64]

inference([inheritance(sport, competition), [1, 0.8]], [inheritance(int_difference(sport, chess), competition), [0, 0.8]], [inheritance(chess, competition), V]). 
V = [1, 0.64] 

inference([inheritance(chess, competition), [0, 0.8]], [inheritance(int_difference(sport, chess), competition), [0, 0.8]], [inheritance(sport, competition), V]). 
V = [0, 0.64] 


%% compound destruction, single premise

inference([inheritance(swan, ext_intersection([swimmer, bird])), [0.9, 0.8]], [inheritance(swan, swimmer), V]).
V = [0.9, 0.72]

inference([inheritance(swan, int_intersection([swimmer, bird])), [0.9, 0.8]], [inheritance(swan, swimmer), V]).
V = [0.9, 0.444444] 

inference([inheritance(swan, ext_difference(swimmer, bird)), [0.9, 0.8]], [inheritance(swan, swimmer), V]).
V = [0.9, 0.72]

inference([inheritance(swan, ext_difference(swimmer, bird)), [0.9, 0.8]], [negation(inheritance(swan, bird)), V]).
V = [0.9, 0.72]

inference([inheritance(int_intersection([sport, chess]), competition), [0.9, 0.8]], [inheritance(sport, competition), V]).
V = [0.9, 0.72] 

inference([inheritance(ext_intersection([sport, chess]), competition), [0.9, 0.8]], [inheritance(sport, competition), V]).
V = [0.9, 0.444444] 

inference([inheritance(int_difference(sport, chess), competition), [0.9, 0.8]], [inheritance(sport, competition), V]).
V = [0.9, 0.72] 

inference([inheritance(int_difference(sport, chess), competition), [0.9, 0.8]], [negation(inheritance(chess, competition)), V]).
V = [0.9, 0.72] 


%% operation on both sides of a relation

inference([inheritance(bird, animal), [0.9, 0.8]], [inheritance(ext_intersection([swimmer, bird]), ext_intersection([swimmer, animal])), V]).
V = [0.9, 0.72] ;

inference([inheritance(ext_intersection([swimmer, bird]), ext_intersection([swimmer, animal])), [0.9, 0.8]], [inheritance(bird, animal), V]).
V = [0.9, 0.444444] ;

inference([inheritance(bird, animal), [0.9, 0.8]], [inheritance(int_intersection([swimmer, bird]), int_intersection([swimmer, animal])), V]).
V = [0.9, 0.72] ;

inference([inheritance(int_intersection([swimmer, bird]), int_intersection([swimmer, animal])), [0.9, 0.8]], [inheritance(bird, animal), V]).
V = [0.9, 0.444444] ;

inference([similarity(bird, animal), [0.9, 0.8]], [similarity(ext_intersection([swimmer, bird]), ext_intersection([swimmer, animal])), V]).
V = [0.9, 0.72] ;

inference([similarity(ext_intersection([swimmer, bird]), ext_intersection([swimmer, animal])), [0.9, 0.8]], [similarity(bird, animal), V]).
V = [0.9, 0.444444] ;

inference([similarity(bird, animal), [0.9, 0.8]], [similarity(int_intersection([swimmer, bird]), int_intersection([swimmer, animal])), V]).
V = [0.9, 0.72] ;

inference([similarity(int_intersection([swimmer, bird]), int_intersection([swimmer, animal])), [0.9, 0.8]], [similarity(bird, animal), V]).
V = [0.9, 0.444444] ;

inference([inheritance(bird, animal), [0.9, 0.8]], [inheritance(ext_difference(bird, swimmer), ext_difference(animal, swimmer)), V]).
V = [0.9, 0.72] ;

inference([inheritance(ext_difference(bird, swimmer), ext_difference(animal, swimmer)), [0.9, 0.8]], [inheritance(bird, animal), V]).
V = [0.9, 0.444444] ;

inference([inheritance(bird, animal), [0.9, 0.8]], [inheritance(int_difference(bird, swimmer), int_difference(animal, swimmer)), V]).
V = [0.9, 0.72] ;

inference([inheritance(int_difference(bird, swimmer), int_difference(animal, swimmer)), [0.9, 0.8]], [inheritance(bird, animal), V]).
V = [0.9, 0.444444] ;

inference([similarity(bird, animal), [0.9, 0.8]], [similarity(ext_difference(bird, swimmer), ext_difference(animal, swimmer)), V]).
V = [0.9, 0.72] ;

inference([similarity(ext_difference(bird, swimmer), ext_difference(animal, swimmer)), [0.9, 0.8]], [similarity(bird, animal), V]).
V = [0.9, 0.444444] ;

inference([similarity(bird, animal), [0.9, 0.8]], [similarity(int_difference(bird, swimmer), int_difference(animal, swimmer)), V]).
V = [0.9, 0.72] ;

inference([similarity(int_difference(bird, swimmer), int_difference(animal, swimmer)), [0.9, 0.8]], [similarity(bird, animal), V]).
V = [0.9, 0.444444] ;

inference([inheritance(bird, animal), [0.9, 0.8]], [inheritance(ext_difference(swimmer, animal), ext_difference(swimmer, bird)), V]).
V = [0.9, 0.72] ;

inference([inheritance(ext_difference(swimmer, animal), ext_difference(swimmer, bird)), [0.9, 0.8]], [inheritance(bird, animal), V]).
V = [0.9, 0.444444] 

inference([inheritance(bird, animal), [0.9, 0.8]], [inheritance(int_difference(swimmer, animal), int_difference(swimmer, bird)), V]).
V = [0.9, 0.72] ;

inference([inheritance(int_difference(swimmer, animal), int_difference(swimmer, bird)), [0.9, 0.8]], [inheritance(bird, animal), V]).
V = [0.9, 0.444444] 

inference([similarity(bird, animal), [0.9, 0.8]], [similarity(ext_difference(swimmer, animal), ext_difference(swimmer, bird)), V]).
V = [0.9, 0.72] ;

inference([similarity(ext_difference(swimmer, animal), ext_difference(swimmer, bird)), [0.9, 0.8]], [similarity(bird, animal), V]).
V = [0.9, 0.444444] 

inference([similarity(bird, animal), [0.9, 0.8]], [similarity(int_difference(swimmer, animal), int_difference(swimmer, bird)), V]).
V = [0.9, 0.72] ;

inference([similarity(int_difference(swimmer, animal), int_difference(swimmer, bird)), [0.9, 0.8]], [similarity(bird, animal), V]).
V = [0.9, 0.444444] 


%% set operations

inference([inheritance(ext_set([earth]), ext_set([venus, mars, pluto])), [0.9, 0.8]], [inheritance(ext_set([earth]), ext_set([pluto, saturn])), [0.7, 0.8]], R).
R = [inheritance(ext_set([earth]), ext_set([pluto])), [0.63, 0.748288]] ;
R = [inheritance(ext_set([earth]), ext_set([venus, mars, pluto, saturn])), [0.97, 0.955648]] ;
R = [inheritance(ext_set([earth]), ext_set([venus, mars])), [0.27, 0.854272]] ;

inference([inheritance(int_set([red, green, blue]), int_set([colorful])), [0.9, 0.8]], [inheritance(int_set([purple, green]), int_set([colorful])), [0.7, 0.8]], R).
R = [inheritance(int_set([green]), int_set([colorful])), [0.63, 0.748288]] ;
R = [inheritance(int_set([red, blue, purple, green]), int_set([colorful])), [0.97, 0.955648]] ;
R = [inheritance(int_set([red, blue]), int_set([colorful])), [0.27, 0.854272]] ;


% ----- NAL-4 ----- %

%% extensional image

inference([inheritance(product([acid, base]), reaction), [1, 0.9]], C).
C = [inheritance(acid, ext_image(reaction, [nil, base])), [1, 0.9]] ;
C = [inheritance(base, ext_image(reaction, [acid, nil])), [1, 0.9]] ;

inference([inheritance(acid, ext_image(reaction, [nil, base])), [1, 0.9]], C).
C = [inheritance(product([acid, base]), reaction), [1, 0.9]] ;

inference([inheritance(acid, ext_image(reaction, [acid, nil])), [1, 0.9]], C).
C = [inheritance(product([acid, acid]), reaction), [1, 0.9]] ;


%% intensional image

inference([inheritance(marry, product([male, female])), [1, 0.9]], C).
C = [inheritance(int_image(marry, [nil, female]), male), [1, 0.9]] ;
C = [inheritance(int_image(marry, [male, nil]), female), [1, 0.9]] ;

inference([inheritance(int_image(marry, [nil, female]), male), [1, 0.9]], C).
C = [inheritance(marry, product([male, female])), [1, 0.9]] ;

inference([inheritance(int_image(marry, [male, nil]), female), [1, 0.9]], C).
C = [inheritance(marry, product([male, female])), [1, 0.9]] ;


%% operation on both sides of a relation

inference([inheritance(bird, animal), [0.9, 0.8]], [inheritance(product([bird, plant]), product([animal, plant])), V]).
V = [0.9, 0.8] ;

inference([inheritance(product([plant, bird]), product([plant, animal])), [0.9, 0.8]], [inheritance(bird, animal), V]).
V = [0.9, 0.8] ;

inference([inheritance(neutralization, reaction), [0.9, 0.8]], [inheritance(ext_image(neutralization, [acid, nil]), ext_image(reaction, [acid, nil])), V]).
V = [0.9, 0.72] ;

inference([inheritance(ext_image(neutralization, [acid, nil]), ext_image(reaction, [acid, nil])), [0.9, 0.8]], [inheritance(neutralization, reaction), V]).
V = [0.9, 0.444444] ;

inference([inheritance(marry, relative),[0.9, 0.8]], [inheritance(int_image(marry, [male, nil]), int_image(relative, [male, nil])), V]).
V = [0.9, 0.72] ;

inference([inheritance(int_image(marry, [male, nil]), int_image(relative, [male, nil])),[0.9, 0.8]], [inheritance(marry, relative), V]).
V = [0.9, 0.444444] ;

inference([inheritance(soda, base), [0.9, 0.8]], [inheritance(ext_image(neutralization, [nil, base]), ext_image(neutralization, [nil, soda])), V]).
V = [0.9, 0.72] ;

inference([inheritance(ext_image(neutralization, [nil, base]), ext_image(neutralization, [nil, soda])), [0.9, 0.8]], [inheritance(soda, base), V]).
V = [0.9, 0.444444] ;

inference([inheritance(male, human),[0.9, 0.8]], [inheritance(int_image(marry, [human, nil]), int_image(marry, [male, nil])), V]).
V = [0.9, 0.72] 

inference([inheritance(int_image(marry, [human, nil]), int_image(marry, [male, nil])),[0.9, 0.8]], [inheritance(male, human), V]).
V = [0.9, 0.444444] 


% ----- NAL-5 ----- %

%% revision

revision([implication(inheritance(robin, flyer), inheritance(robin, bird)), [1, 0.8]], [implication(inheritance(robin, flyer), inheritance(robin, bird)), [0, 0.5]], R).
R = [implication(inheritance(robin, flyer), inheritance(robin, bird)), [0.8, 0.833333]] 

revision([equivalence(inheritance(robin, flyer), inheritance(robin, bird)), [1, 0.8]], [equivalence(inheritance(robin, flyer), inheritance(robin, bird)), [0, 0.5]], R).
R = [equivalence(inheritance(robin, flyer), inheritance(robin, bird)), [0.8, 0.833333]] ;


%% choice

choice([implication(inheritance(robin, flyer), inheritance(robin, bird)), [1, 0.8]], [implication(inheritance(robin, flyer), inheritance(robin, bird)), [0, 0.5]], R).
R = [implication(inheritance(robin, flyer), inheritance(robin, bird)), [1, 0.8]] 

choice([implication(inheritance(robin, flyer), inheritance(robin, bird)), [0.8, 0.9]], [implication(inheritance(robin, swimmer), inheritance(robin, bird)), [1, 0.5]], R).
R = [implication(inheritance(robin, flyer), inheritance(robin, bird)), [0.8, 0.9]] ;


%% deduction

inference([implication(inheritance(robin, bird), inheritance(robin, animal)), [0.9, 0.8]], [implication(inheritance(robin, flyer), inheritance(robin, bird)), [1, 0.5]], R).
R = [implication(inheritance(robin, flyer), inheritance(robin, animal)), [0.9, 0.36]] ;

inference([equivalence(inheritance(robin, bird), inheritance(robin, animal)), [0.9, 0.8]], [equivalence(inheritance(robin, flyer), inheritance(robin, bird)), [1, 0.5]], R).
R = [equivalence(inheritance(robin, flyer), inheritance(robin, animal)), [0.9, 0.4]] ;


%% induction

inference([implication(inheritance(robin, bird), inheritance(robin, animal)), [0.9, 0.8]], [implication(inheritance(robin, bird), inheritance(robin, flyer)), [1, 0.5]], R).
R = [implication(inheritance(robin, flyer), inheritance(robin, animal)), [0.9, 0.28]] ;


%% abduction

inference([implication(inheritance(robin, bird), inheritance(robin, animal)), [0.9, 0.8]], [implication(inheritance(robin, flyer), inheritance(robin, animal)), [1, 0.5]], R).
R = [implication(inheritance(robin, flyer), inheritance(robin, bird)), [1, 0.264706]] ;


%% examplification

inference([implication(inheritance(robin, flyer), inheritance(robin, bird)), [0.9, 0.8]], [implication(inheritance(robin, bird), inheritance(robin, animal)), [1, 0.5]], R).
R = [implication(inheritance(robin, animal), inheritance(robin, flyer)), [1, 0.264706]] ;


%% convension --- the current version contains a bug to be fixed

inference([implication(inheritance(robin, flyer), inheritance(robin, animal)), [0.9, 0.8]], R).
R = [implication(inheritance(robin, animal), inheritance(robin, flyer)), [1, 0.418605]] ;

inference([equivalence(inheritance(robin, flyer), inheritance(robin, bird)), [0.9, 0.8]], [implication(inheritance(robin, flyer), inheritance(robin, bird)), V]).
V = [0.9, 0.72]

inference([implication(inheritance(robin, flyer), inheritance(robin, bird)), [0.9, 0.8]], [implication(inheritance(robin, bird), inheritance(robin, flyer)), [0.9, 0.8]], R).
R = [equivalence(inheritance(robin, flyer), inheritance(robin, bird)), [0.81, 0.695296]] ;


%% comparison

inference([implication(inheritance(robin, bird), inheritance(robin, animal)), [0.9, 0.8]], [implication(inheritance(robin, bird), inheritance(robin, flyer)), [0.9, 0.8]], R).
R = [equivalence(inheritance(robin, flyer), inheritance(robin, animal)), [0.818182, 0.387855]] ;

inference([implication(inheritance(robin, bird), inheritance(robin, animal)), [0.9, 0.8]], [implication(inheritance(robin, flyer), inheritance(robin, animal)), [0.9, 0.8]], R).
R = [equivalence(inheritance(robin, flyer), inheritance(robin, bird)), [0.818182, 0.387855]] ;


%% analogy

inference([implication(inheritance(robin, bird), inheritance(robin, animal)), [0.9, 0.8]], [equivalence(inheritance(robin, flyer), inheritance(robin, animal)), [0.9, 0.8]], R).
R = [implication(inheritance(robin, bird), inheritance(robin, flyer)), [0.81, 0.41472]] ;

inference([implication(inheritance(robin, bird), inheritance(robin, animal)), [0.9, 0.8]], [equivalence(inheritance(robin, flyer), inheritance(robin, bird)), [0.9, 0.8]], R).
R = [implication(inheritance(robin, flyer), inheritance(robin, animal)), [0.81, 0.41472]] ;



%% compound construction, two premises

inference([implication(inheritance(robin, bird), inheritance(robin, animal)), [0.9, 0.8]], [implication(inheritance(robin, bird), inheritance(robin, flyer)), [0.9, 0.8]], R).
R = [implication(inheritance(robin, bird), conjunction([inheritance(robin, animal), inheritance(robin, flyer)])), [0.81, 0.695296]] ;
R = [implication(inheritance(robin, bird), disjunction([inheritance(robin, animal), inheritance(robin, flyer)])), [0.99, 0.971776]] ;

inference([implication(inheritance(robin, bird), inheritance(robin, animal)), [0.9, 0.8]], [implication(inheritance(robin, flyer), inheritance(robin, animal)), [0.9, 0.8]], R).
R = [implication(disjunction([inheritance(robin, bird), inheritance(robin, flyer)]), inheritance(robin, animal)), [0.81, 0.695296]] ;
R = [implication(conjunction([inheritance(robin, bird), inheritance(robin, flyer)]), inheritance(robin, animal)), [0.99, 0.971776]] ;

inference([inheritance(robin, animal), [0.9, 0.9]], [inheritance(robin, flyer), [0.9, 0.9]], [conjunction([inheritance(robin, animal), inheritance(robin, flyer)]), V]).
V = [0.81, 0.842661] ;

inference([inheritance(robin, animal), [0.9, 0.8]], [inheritance(robin, flyer), [0.9, 0.8]], [disjunction([inheritance(robin, animal), inheritance(robin, flyer)]), V]).
V = [0.99, 0.971776] ;


%% compound construction, single premise

inference([implication(inheritance(robin, bird), inheritance(robin, animal)), [0.9, 0.8]], [implication(inheritance(robin, bird), conjunction([inheritance(robin, animal), inheritance(robin, flyer)])), V]).
V = [0.9, 0.444444] ;

inference([implication(inheritance(robin, bird), inheritance(robin, animal)), [0.9, 0.8]], [implication(inheritance(robin, bird), disjunction([inheritance(robin, animal), inheritance(robin, flyer)])), V]).
V = [0.9, 0.72] ;

inference([implication(inheritance(robin, bird), inheritance(robin, animal)), [0.9, 0.8]], [implication(disjunction([inheritance(robin, bird), inheritance(robin, flyer)]), inheritance(robin, animal)), V]).
V = [0.9, 0.444444] ;

inference([implication(inheritance(robin, bird), inheritance(robin, animal)), [0.9, 0.8]], [implication(conjunction([inheritance(robin, bird), inheritance(robin, flyer)]), inheritance(robin, animal)), V]).
V = [0.9, 0.72] ;

inference([inheritance(robin, animal), [0.9, 0.8]], [conjunction([inheritance(robin, animal), inheritance(robin, flyer)]), V]).
V = [0.9, 0.444444] 

inference([inheritance(robin, animal), [0.9, 0.8]], [disjunction([inheritance(robin, animal), inheritance(robin, flyer)]), V]).
V = [0.9, 0.72] ;


%% compound destruction, two premises

inference([implication(inheritance(robin, bird), inheritance(robin, flyer)), [1, 0.8]], [implication(inheritance(robin, bird), conjunction([inheritance(robin, animal), inheritance(robin, flyer)])), [0, 0.8]], R).
R = [implication(inheritance(robin, bird), inheritance(robin, animal)), [0, 0.64]]

inference([implication(inheritance(robin, bird), inheritance(robin, flyer)), [0, 0.8]], [implication(inheritance(robin, bird), disjunction([inheritance(robin, animal), inheritance(robin, flyer)])), [1, 0.8]], R).
R = [implication(inheritance(robin, bird), inheritance(robin, animal)), [1, 0.64]]

inference([implication(inheritance(robin, bird), inheritance(robin, animal)), [1, 0.8]], [implication(disjunction([inheritance(robin, bird), inheritance(robin, flyer)]), inheritance(robin, animal)), [0, 0.8]], R).
R = [implication(inheritance(robin, flyer), inheritance(robin, animal)), [0, 0.64]]

inference([implication(inheritance(robin, bird), inheritance(robin, animal)), [0, 0.8]], [implication(conjunction([inheritance(robin, bird), inheritance(robin, flyer)]), inheritance(robin, animal)), [1, 0.8]], R).
R = [implication(inheritance(robin, flyer), inheritance(robin, animal)), [1, 0.64]] 

inference([inheritance(robin, bird), [1, 0.8]], [conjunction([inheritance(robin, bird), inheritance(robin, flyer)]), [0, 0.8]], R).
R = [inheritance(robin, flyer), [0, 0.64]] ;

inference([inheritance(robin, bird), [0, 0.8]], [disjunction([inheritance(robin, bird), inheritance(robin, flyer)]), [1, 0.8]], R).
R = [inheritance(robin, flyer), [1, 0.64]] ;


%% compound destruction, single premise

inference([implication(inheritance(robin, bird), conjunction([inheritance(robin, animal), inheritance(robin, flyer)])), [0.9, 0.8]], [implication(inheritance(robin, bird), inheritance(robin, animal)), V]).
V = [0.9, 0.72] ;

inference([implication(inheritance(robin, bird), disjunction([inheritance(robin, animal), inheritance(robin, flyer)])), [0.9, 0.8]], [implication(inheritance(robin, bird), inheritance(robin, animal)), V]).
V = [0.9, 0.444444] ;

inference([implication(disjunction([inheritance(robin, bird), inheritance(robin, flyer)]), inheritance(robin, animal)), [0.9, 0.8]], [implication(inheritance(robin, bird), inheritance(robin, animal)), V]).
V = [0.9, 0.72] ;

inference([implication(conjunction([inheritance(robin, bird), inheritance(robin, flyer)]), inheritance(robin, animal)), [0.9, 0.8]], [implication(inheritance(robin, bird), inheritance(robin, animal)), V]).
V = [0.9, 0.444444] 

inference([conjunction([inheritance(robin, bird), inheritance(robin, flyer)]), [0.9, 0.8]], [inheritance(robin, bird),V]).
V = [0.9, 0.72] ;

inference([disjunction([inheritance(robin, bird), inheritance(robin, flyer)]), [0.9, 0.8]], [inheritance(robin, bird),V]).
V = [0.9, 0.444444] ;


%% operation on both sides of a relation

inference([implication(p, q), [0.9, 0.8]], [implication(conjunction([p, r]), conjunction([q, r])), V]).
V = [0.9, 0.72] ;

inference([implication(conjunction([p, r]), conjunction([q, r])), [0.9, 0.8]], [implication(p, q), V]).
V = [0.9, 0.444444] ;

inference([implication(p, q), [0.9, 0.8]], [implication(disjunction([p, r]), disjunction([q, r])), V]).
V = [0.9, 0.72] ;

inference([implication(disjunction([p, r]), disjunction([q, r])), [0.9, 0.8]], [implication(p, q), V]).
V = [0.9, 0.444444] ;

inference([equivalence(p, q), [0.9, 0.8]], [equivalence(conjunction([p, r]), conjunction([q, r])), V]).
V = [0.9, 0.72] ;

inference([equivalence(conjunction([p, r]), conjunction([q, r])), [0.9, 0.8]], [equivalence(p, q), V]).
V = [0.9, 0.444444] ;

inference([equivalence(p, q), [0.9, 0.8]], [equivalence(disjunction([p, r]), disjunction([q, r])), V]).
V = [0.9, 0.72] ;

inference([equivalence(disjunction([p, r]), disjunction([q, r])), [0.9, 0.8]], [equivalence(p, q), V]).
V = [0.9, 0.444444] ;


%% negation

inference([negation(inheritance(robin, bird)), [0.9, 0.8]], R).
R = [inheritance(robin, bird), [0.1, 0.8]] ;

inference([inheritance(robin, bird), [0.2, 0.8]], [negation(inheritance(robin, bird)), V]).
V = [0.8, 0.8] ;

inference([implication(negation(inheritance(penguin, flyer)), inheritance(penguin, swimmer)), [0.1, 0.8]], R).
R = [implication(negation(inheritance(penguin, swimmer)), inheritance(penguin, flyer)), [0, 0.418605]] ;


%% conditional inference

inference([implication(inheritance(robin, bird), inheritance(robin, animal)), [0.9, 0.8]], [inheritance(robin, bird), [1, 0.5]], R).
R = [inheritance(robin, animal), [0.9, 0.36]] ;

inference([implication(inheritance(robin, bird), inheritance(robin, animal)), [0.9, 0.8]], [inheritance(robin, animal), [1, 0.5]], R).
R = [inheritance(robin, bird), [1, 0.264706]] ;

inference([inheritance(robin, animal), [0.9, 0.8]], [inheritance(robin, flyer), [1, 0.5]], [implication(inheritance(robin, flyer), inheritance(robin, animal)), V]).
V = [0.9, 0.285714] ;

inference([inheritance(robin, animal), [1, 0.5]], [equivalence(inheritance(robin, flyer), inheritance(robin, animal)), [0.9, 0.8]], R).
R = [inheritance(robin, flyer), [0.9, 0.2592]] ;

inference([inheritance(robin, animal), [0.9, 0.8]], [inheritance(robin, flyer), [1, 0.5]], [equivalence(inheritance(robin, flyer), inheritance(robin, animal)), V]).
V = [0.9, 0.285714] ;

inference([implication(conjunction([a1, a2, a3]), c), [0.9, 0.9]], [a2, [0.9, 0.9]], R).
R = [implication(conjunction([a1, a3]), c), [0.81, 0.6561]] ;

inference([implication(conjunction([a1, a2, a3]), c), [0.9, 0.9]], [implication(conjunction([a1, a3]), c), [0.9, 0.9]], R).
R = [a2, [0.9, 0.421631]]

inference([implication(conjunction([a1, a3]), c), [0.9, 0.9]], [a2, [0.9, 0.9]], [implication(conjunction([a2, a1, a3]), c), V]).
V = [0.9, 0.421631] ;

inference([implication(conjunction([a1, a2, a3]), c), [0.9, 0.9]], [implication(b2, a2), [0.9, 0.9]], R).
R = [implication(conjunction([a1, b2, a3]), c), [0.81, 0.6561]] ;

inference([implication(conjunction([a1, a2, a3]), c), [0.9, 0.9]], [implication(conjunction([a1, b2, a3]), c), [0.9, 0.9]], R).
R = [implication(b2, a2), [0.9, 0.421631]] ;

inference([implication(conjunction([a1, b2, a3]), c), [0.9, 0.9]], [implication(b2, a2), [0.9, 0.9]], R).
R = [implication(conjunction([a1, a2, a3]), c), [0.9, 0.421631]] ;


% ----- NAL-6 ----- %

%% variable unification

revision([implication(inheritance(X, bird), inheritance(X, flyer)), [0.9, 0.8]], [implication(inheritance(Y, bird), inheritance(Y, flyer)), [1, 0.5]], R).
R = [implication(inheritance(_G157, bird), inheritance(_G157, flyer)), [0.92, 0.833333]] ;

inference([implication(inheritance(X, bird), inheritance(X, animal)), [1, 0.9]], [implication(inheritance(Y, robin), inheritance(Y, bird)), [1, 0.9]], R).
R = [implication(inheritance(_G160, robin), inheritance(_G160, animal)), [1, 0.81]] ;

inference([implication(inheritance(X, bird), inheritance(X, animal)), [1, 0.9]], [implication(inheritance(Y, robin), inheritance(Y, animal)), [1, 0.9]], R).
R = [implication(inheritance(_G160, robin), inheritance(_G160, bird)), [1, 0.447514]] ;

inference([implication(inheritance(X, robin), inheritance(X, animal)), [1, 0.9]], [implication(inheritance(Y, robin), inheritance(Y, bird)), [1, 0.9]], R).
R = [implication(inheritance(_G160, bird), inheritance(_G160, animal)), [1, 0.447514]] ;

inference([implication(inheritance(X, feathered), inheritance(X, bird)), [1, 0.9]], [equivalence(inheritance(Y, flyer), inheritance(Y, bird)), [1, 0.9]], R).
R = [implication(inheritance(_G157, feathered), inheritance(_G157, flyer)), [1, 0.729]] ;

inference([implication(inheritance(X, feathered), inheritance(X, flyer)), [1, 0.9]], [implication(inheritance(Y, feathered), inheritance(Y, bird)), [1, 0.9]], R).
R = [implication(inheritance(_G160, bird), inheritance(_G160, flyer)), [1, 0.447514]] 

inference([implication(conjunction([inheritance(X, feathered), inheritance(X, flyer)]), inheritance(X, bird)), [1, 0.9]], [implication(inheritance(Y, swimmer), inheritance(Y, feathered)), [1, 0.9]], R).
R = [implication(conjunction([inheritance(_G160, swimmer), inheritance(_G160, flyer)]), inheritance(_G160, bird)), [1, 0.81]] ;

inference([implication(conjunction([inheritance(X, feathered), inheritance(X, flyer)]), inheritance(X, bird)), [1, 0.9]], [implication(conjunction([inheritance(X, swimmer), inheritance(X, flyer)]), inheritance(X, bird)), [1, 0.9]], R).
R = [implication(inheritance(_G160, swimmer), inheritance(_G160, feathered)), [1, 0.447514]] 

inference([implication(conjunction([inheritance(X, swimmer), inheritance(X, flyer)]), inheritance(X, bird)), [1, 0.9]], [implication(inheritance(Y, swimmer), inheritance(Y, feathered)), [1, 0.9]], R).
R = [implication(conjunction([inheritance(_G160, feathered), inheritance(_G160, flyer)]), inheritance(_G160, bird)), [1, 0.447514]] 

inference([implication(conjunction([inheritance(X, feathered), inheritance(X, flyer)]), inheritance(X, bird)), [1, 0.9]], [implication(inheritance(Y, swimmer), inheritance(Y, feathered)), [1, 0.9]], R).
R = [implication(conjunction([inheritance(_G157, swimmer), inheritance(_G157, flyer)]), inheritance(_G157, bird)), [0.81, 0.5184]] ;


%% variable elimination

inference([implication(inheritance(X, bird), inheritance(X, animal)), [1, 0.9]], [inheritance(robin, bird), [1, 0.9]], R).
R = [inheritance(robin, animal), [1, 0.81]] ;

inference([implication(inheritance(X, bird), inheritance(X, animal)), [1, 0.9]], [inheritance(robin, animal), [1, 0.9]], R).
R = [inheritance(robin, bird), [1, 0.447514]] ;

inference([inheritance(robin, animal), [1, 0.9]], [equivalence(inheritance(X, bird), inheritance(X, animal)), [1, 0.9]], R).
R = [inheritance(robin, bird), [1, 0.729]] ;

inference([implication(conjunction([inheritance(X, feathered), inheritance(X, flyer)]), inheritance(X, bird)), [1, 0.9]], [inheritance(swan, feathered), [1, 0.9]], R).
R = [implication(inheritance(swan, flyer), inheritance(swan, bird)), [1, 0.81]] ;

inference([conjunction([inheritance(var(X, []), bird), inheritance(var(X, []), swimmer)]), [1, 0.9]], [inheritance(swan, bird), [1, 0.9]], R).
R = [inheritance(swan, swimmer), [1, 0.447514]] 

inference([conjunction([inheritance(var(X, []), flyer), inheritance(var(X, []), bird), inheritance(var(X, []), swimmer)]), [1, 0.9]], [inheritance(swan, bird), [1, 0.9]], R).
R = [conjunction([inheritance(swan, flyer), inheritance(swan, swimmer)]), [1, 0.447514]] ;


%% variable introduction

inference([inheritance(robin, animal), [1, 0.9]], [inheritance(robin, bird), [1, 0.9]], R).
R = [implication(inheritance(_G292, bird), inheritance(_G292, animal)), [1, 0.447514]] ;
R = [equivalence(inheritance(_G292, bird), inheritance(_G292, animal)), [1, 0.447514]] ;
R = [conjunction([inheritance(var(_G297, []), bird), inheritance(var(_G297, []), animal)]), [1, 0.81]] ;

inference([inheritance(sport, competition), [1, 0.9]], [inheritance(chess, competition), [1, 0.9]], R).
R = [implication(inheritance(sport, _G293), inheritance(chess, _G293)), [1, 0.447514]] ;
R = [equivalence(inheritance(sport, _G293), inheritance(chess, _G293)), [1, 0.447514]] ;
R = [conjunction([inheritance(chess, var(_G297, [])), inheritance(sport, var(_G297, []))]), [1, 0.81]] ;


%% multiple variables

inference([inheritance(key1, ext_image(open, [nil, lock1])), [1, 0.9]], [inheritance(key1, key), [1, 0.9]],  R).
R = [implication(inheritance(_G310, key), inheritance(_G310, ext_image(open, [nil, lock1]))), [1, 0.447514]] ;
R = [conjunction([inheritance(var(_G315, []), key), inheritance(var(_G315, []), ext_image(open, [nil, lock1]))]), [1, 0.81]] ;

inference([implication(inheritance(X, key), inheritance(lock1, ext_image(open, [X, nil]))), [1, 0.9]], [inheritance(lock1, lock), [1, 0.9]],  R).
R = [implication(conjunction([inheritance(_G160, key), inheritance(_G345, lock)]), inheritance(_G345, ext_image(open, [_G160, nil]))), [1, 0.447514]] ;
R = [conjunction([implication(inheritance(_G160, key), inheritance(var(_G345, []), ext_image(open, [_G160, nil]))), inheritance(var(_G345, []), lock)]), [1, 0.81]] ;

inference([conjunction([inheritance(var(X, []), key), inheritance(lock1, ext_image(open, [var(X, []), nil]))]), [1, 0.9]],[inheritance(lock1, lock), [1, 0.9]],  R).
R = [implication(inheritance(_G359, lock), conjunction([inheritance(_G359, ext_image(open, [var(_G160, [_G359]), nil])), inheritance(var(_G160, [_G359]), key)])), [1, 0.447514]] ;
R = [conjunction([inheritance(var(_G364, []), lock), inheritance(var(_G364, []), ext_image(open, [var(_G160, []), nil])), inheritance(var(_G160, []), key)]), [1, 0.81]] ;