2% nal.pl
    3% Non-Axiomatic Logic in Prolog
    4% Version: 1.1, September 2012
    5% GNU Lesser General Public License
    6% Author: Pei Wang
    7
    8:-module(nal,[]).    9
   10:- set_module(class(library)).   11:- set_module(base(system)).   12
   13
   14use_nars_config_info(List):- is_list(List),!,maplist(use_nars_config_info, List).
   15use_nars_config_info([]):-!.
   16use_nars_config_info(element(_,[], List)):-!, use_nars_config_info(List).
   17use_nars_config_info(element(_,[name=Name,value=Value], _)):-!,
   18 use_nars_config_info(Name=Value).
   19use_nars_config_info(Name=Value):-  string(Name), downcase_atom(Name,NameD),   NameD\=Name,!,use_nars_config_info(NameD=Value).
   20use_nars_config_info(Name=Value):- string(Value), downcase_atom(Value,ValueD),ValueD\=Value,!,use_nars_config_info(Name=ValueD).
   21use_nars_config_info(Name=Value):- atom(Value), atom_number(Value,Number), use_nars_config_info(Name=Number).
   22%use_nars_config_info(Ignore):- string(Ignore),!.
   23%use_nars_config_info(NameValue):- dmsg(use_nars_config_info(NameValue)),fail.
   24use_nars_config_info(Name=Value):- number(Value), !, nb_setval(Name,Value).
   25use_nars_config_info(Name=Value):- nb_setval(Name, Value).
   26use_nars_config_info(_).
   27
   28% default gobals
   29:-  use_nars_config_info(volume=100).   30:-  use_nars_config_info(novelty_horizon=100000).   31:-  use_nars_config_info(decision_threshold=0.51).   32:-  use_nars_config_info(concept_bag_size=80000).   33:-  use_nars_config_info(concept_bag_levels=1000).   34:-  use_nars_config_info(duration=5).   35:-  use_nars_config_info(horizon=1).   36:-  use_nars_config_info(truth_epsilon=0.01).   37:-  use_nars_config_info(budget_epsilon=0.0001).   38:-  use_nars_config_info(budget_threshold=0.01).   39:-  use_nars_config_info(default_confirmation_expectation=0.6).   40:-  use_nars_config_info(always_create_concept=true).   41:-  use_nars_config_info(default_creation_expectation=0.66).   42:-  use_nars_config_info(default_creation_expectation_goal=0.6).   43:-  use_nars_config_info(default_judgment_confidence=0.9).   44:-  use_nars_config_info(default_judgment_priority=0.8).   45:-  use_nars_config_info(default_judgment_durability=0.5).   46:-  use_nars_config_info(default_question_priority=0.9).   47:-  use_nars_config_info(default_question_durability=0.9).   48:-  use_nars_config_info(default_goal_confidence=0.9).   49:-  use_nars_config_info(default_goal_priority=0.9).   50:-  use_nars_config_info(default_goal_durability=0.9).   51:-  use_nars_config_info(default_quest_priority=0.9).   52:-  use_nars_config_info(default_quest_durability=0.9).   53:-  use_nars_config_info(bag_threshold=1.0).   54:-  use_nars_config_info(forget_quality_relative=0.3).   55:-  use_nars_config_info(revision_max_occurrence_distance=10).   56:-  use_nars_config_info(task_link_bag_size=100).   57:-  use_nars_config_info(task_link_bag_levels=10).   58:-  use_nars_config_info(term_link_bag_size=100).   59:-  use_nars_config_info(term_link_bag_levels=10).   60:-  use_nars_config_info(term_link_max_matched=10).   61:-  use_nars_config_info(novel_task_bag_size=1000).   62:-  use_nars_config_info(novel_task_bag_levels=100).   63:-  use_nars_config_info(novel_task_bag_selections=100).   64:-  use_nars_config_info(sequence_bag_size=30).   65:-  use_nars_config_info(sequence_bag_levels=10).   66:-  use_nars_config_info(operation_bag_size=10).   67:-  use_nars_config_info(operation_bag_levels=10).   68:-  use_nars_config_info(operation_samples=6).   69:-  use_nars_config_info(projection_decay=0.1).   70:-  use_nars_config_info(maximum_evidental_base_length=20000).   71:-  use_nars_config_info(termlink_max_reasoned=3).   72:-  use_nars_config_info(term_link_record_length=10).   73:-  use_nars_config_info(concept_beliefs_max=28).   74:-  use_nars_config_info(concept_questions_max=5).   75:-  use_nars_config_info(concept_goals_max=7).   76:-  use_nars_config_info(reliance=0.9).   77:-  use_nars_config_info(discount_rate=0.5).   78:-  use_nars_config_info(immediate_eternalization=true).   79:-  use_nars_config_info(sequence_bag_attempts=10).   80:-  use_nars_config_info(condition_bag_attempts=10).   81:-  use_nars_config_info(derivation_priority_leak=0.4).   82:-  use_nars_config_info(derivation_durability_leak=0.4).   83:-  use_nars_config_info(curiosity_desire_confidence_mul=0.1).   84:-  use_nars_config_info(curiosity_desire_priority_mul=0.1).   85:-  use_nars_config_info(curiosity_desire_durability_mul=0.3).   86:-  use_nars_config_info(curiosity_for_operator_only=false).   87:-  use_nars_config_info(break_nal_hol_boundary=false).   88:-  use_nars_config_info(question_generation_on_decision_making=false).   89:-  use_nars_config_info(how_question_generation_on_decision_making=false).   90:-  use_nars_config_info(anticipation_confidence=0.1).   91:-  use_nars_config_info(anticipation_tolerance=100.0).   92:-  use_nars_config_info(retrospective_anticipations=false).   93:-  use_nars_config_info(satisfaction_treshold=0.0).   94:-  use_nars_config_info(complexity_unit=1.0).   95:-  use_nars_config_info(interval_adapt_speed=4.0).   96:-  use_nars_config_info(tasklink_per_content=4).   97:-  use_nars_config_info(default_feedback_priority=0.9).   98:-  use_nars_config_info(default_feedback_durability=0.5).   99:-  use_nars_config_info(concept_forget_durations=2.0).  100:-  use_nars_config_info(termlink_forget_durations=10.0).  101:-  use_nars_config_info(tasklink_forget_durations=4.0).  102:-  use_nars_config_info(event_forget_durations=4.0).  103:-  use_nars_config_info(variable_introduction_combinations_max=8).  104:-  use_nars_config_info(variable_introduction_confidence_mul=0.9).  105:-  use_nars_config_info(anticipations_per_concept_max=8).  106:-  use_nars_config_info(motor_babbling_confidence_threshold=0.8).  107:-  use_nars_config_info(threads_amount=1).  108:-  use_nars_config_info(milliseconds_per_step=0).  109:-  use_nars_config_info(steps_clock=true).  110:-  use_nars_config_info(derivation_durability_leak=0.4).  111:-  use_nars_config_info(derivation_priority_leak=0.4).  112
  113use_nars_config(File):- (\+ atom(File); \+ is_absolute_file_name(File)),
  114  absolute_file_name(File,Absolute), !, use_nars_config(Absolute).
  115use_nars_config(Absolute):- open(Absolute,read,In),
  116   load_sgml(In, Dom,
  117                  [  dialect(html5),
  118                     attribute_value(string),
  119                     cdata(string),
  120                     system_entities(true),
  121                     space(remove),
  122                     syntax_errors(quiet),
  123                     case_preserving_attributes(false),
  124                     case_sensitive_attributes(false),
  125                  max_errors(-1)]),!,
  126   close(In),
  127   use_nars_config_info(Dom),!.
  128
  129parse_config:-
  130  use_nars_config(library('../config/mvpConfig.xml')).
  131
  132
  133
  134% This program covers the inference rules of upto NAL-6 in
  135% "Non-Axiomatic Logic: A Model of Intelligent Reasoning"
  136% For the details of syntax, see the "User's Guide of NAL"
  137
  138%%% individual inference rules
  139
  140% There are three types of inference rules in NAL:
  141% (1) "revision" merges its two premises into a conclusion;
  142% (2) "choice" selects one of its two premises as a conclusion;
  143% (3) "inference" generates a conclusion from one or two premises.
  144
  145% revision
  146
  147revision([S, T1], [S, T2], [S, T]) :-
  148	nal_f_rev(T1, T2, T).
  149
  150% choice
  151
  152choice([S, [F1, C1]], [S, [_F2, C2]], [S, [F1, C1]]) :-
  153	C1 >= C2, !.
  154choice([S, [_F1, C1]], [S, [F2, C2]], [S, [F2, C2]]) :-
  155	C1 < C2, !.
  156choice([S1, T1], [S2, T2], [S1, T1]) :-
  157	S1 \= S2, nal_f_exp(T1, E1), nal_f_exp(T2, E2), E1 >= E2, !.
  158choice([S1, T1], [S2, T2], [S2, T2]) :-
  159	S1 \= S2, nal_f_exp(T1, E1), nal_f_exp(T2, E2), E1 < E2, !.
  160
  161% simplified version
  162
  163infer(T1, T) :- inference([T1, [1, 0.9]], T).
  164
  165infer(inheritance(W1, ext_image(ext_image(represent, [nil, inheritance(product([X, T2]), R)]), [nil, W2, W3])), inheritance(W1, ext_image(represent, [nil, X])), [inheritance(ext_image(represent, [nil, Y]), ext_image(ext_image(represent, [nil, inheritance(product([Y, T2]), R)]), [nil, W2, W3])), V])  :- nal_f_ind([1, 0.9], [1, 0.9], V), !.
  166
  167infer(inheritance(W3, ext_image(ext_image(represent, [nil, inheritance(product([T1, X]), R)]), [W1, W2, nil])), inheritance(W3, ext_image(represent, [nil, X])), [inheritance(ext_image(represent, [nil, Y]), ext_image(ext_image(represent, [nil, inheritance(product([T1, Y]), R)]), [W1, W2, nil])), V])  :- nal_f_ind([1, 0.9], [1, 0.9], V), !.
  168
  169infer(T1, T2, T) :- inference([T1, [1, 0.9]], [T2, [1, 0.9]], T).
  170
  171
  172% inference/2
  176inference([inheritance(S, P), T1], [inheritance(P, S), T]) :-
  177	nal_f_cnv(T1, T).
  178inference([implication(S, P), T1], [implication(P, S), T]) :-
  179	nal_f_cnv(T1, T).
  180inference([implication(negation(S), P), T1], [implication(negation(P), S), T]) :-
  181	nal_f_cnt(T1, T).
  182
  183inference([negation(S), T1], [S, T]) :-
  184	nal_f_neg(T1, T).
  185inference([S, [F1, C1]], [negation(S), T]) :-
  186	F1 < 0.5, nal_f_neg([F1, C1], T).
  190inference([S1, T], [S, T]) :-
  191	nal_reduce(S1, S), S1 \== S, !.
  192inference([S1, T], [S, T]) :-
  193	equivalence(S1, S); equivalence(S, S1).
  194
  195inference(P, C) :-
  196	inference(P, [S, [1, 1]], C), call(S).
  197inference(P, C) :-
  198	inference([S, [1, 1]], P, C), call(S).
  199
  200
  201% inference/3
  205inference([inheritance(M, P), T1], [inheritance(S, M), T2], [inheritance(S, P), T]) :-
  206	S \= P, nal_f_ded(T1, T2, T).
  207inference([inheritance(P, M), T1], [inheritance(S, M), T2], [inheritance(S, P), T]) :-
  208	S \= P, nal_f_abd(T1, T2, T).
  209inference([inheritance(M, P), T1], [inheritance(M, S), T2], [inheritance(S, P), T]) :-
  210	S \= P, nal_f_ind(T1, T2, T).
  211inference([inheritance(P, M), T1], [inheritance(M, S), T2], [inheritance(S, P), T]) :-
  212	S \= P, nal_f_exe(T1, T2, T).
  216inference([inheritance(S, P), T1], [inheritance(P, S), T2], [similarity(S, P), T]) :-
  217	nal_f_int(T1, T2, T).
  221inference([inheritance(P, M), T1], [inheritance(S, M), T2], [similarity(S, P), T]) :-
  222	S \= P, nal_f_com(T1, T2, T).
  223inference([inheritance(M, P), T1], [inheritance(M, S), T2], [similarity(S, P), T]) :-
  224	S \= P, nal_f_com(T1, T2, T).
  225inference([inheritance(M, P), T1], [similarity(S, M), T2], [inheritance(S, P), T]) :-
  226	S \= P, nal_f_ana(T1, T2, T).
  227inference([inheritance(P, M), T1], [similarity(S, M), T2], [inheritance(P, S), T]) :-
  228	S \= P, nal_f_ana(T1, T2, T).
  229inference([similarity(M, P), T1], [similarity(S, M), T2], [similarity(S, P), T]) :-
  230	S \= P, nal_f_res(T1, T2, T).
  234inference([inheritance(P, M), T1], [inheritance(S, M), T2], [inheritance(N, M), T]) :-
  235	S \= P, nal_reduce(int_intersection([P, S]), N), nal_f_int(T1, T2, T).
  236inference([inheritance(P, M), T1], [inheritance(S, M), T2], [inheritance(N, M), T]) :-
  237	S \= P, nal_reduce(ext_intersection([P, S]), N), nal_f_uni(T1, T2, T).
  238inference([inheritance(P, M), T1], [inheritance(S, M), T2], [inheritance(N, M), T]) :-
  239	S \= P, nal_reduce(int_difference(P, S), N), nal_f_dif(T1, T2, T).
  240inference([inheritance(M, P), T1], [inheritance(M, S), T2], [inheritance(M, N), T]) :-
  241	S \= P, nal_reduce(ext_intersection([P, S]), N), nal_f_int(T1, T2, T).
  242inference([inheritance(M, P), T1], [inheritance(M, S), T2], [inheritance(M, N), T]) :-
  243	S \= P, nal_reduce(int_intersection([P, S]), N), nal_f_uni(T1, T2, T).
  244inference([inheritance(M, P), T1], [inheritance(M, S), T2], [inheritance(M, N), T]) :-
  245	S \= P, nal_reduce(ext_difference(P, S), N), nal_f_dif(T1, T2, T).
  249inference([inheritance(S, M), T1], [inheritance(int_intersection(L), M), T2], [inheritance(P, M), T]) :-
  250	ground(S), ground(L), member(S, L), delete(L, S, N), nal_reduce(int_intersection(N), P), nal_f_pnn(T1, T2, T).
  251inference([inheritance(S, M), T1], [inheritance(ext_intersection(L), M), T2], [inheritance(P, M), T]) :-
  252	ground(S), ground(L), member(S, L), delete(L, S, N), nal_reduce(ext_intersection(N), P), nal_f_npp(T1, T2, T).
  253inference([inheritance(S, M), T1], [inheritance(int_difference(S, P), M), T2], [inheritance(P, M), T]) :-
  254	atom(S), atom(P), nal_f_pnp(T1, T2, T).
  255inference([inheritance(S, M), T1], [inheritance(int_difference(P, S), M), T2], [inheritance(P, M), T]) :-
  256	atom(S), atom(P), nal_f_nnn(T1, T2, T).
  257inference([inheritance(M, S), T1], [inheritance(M, ext_intersection(L)), T2], [inheritance(M, P), T]) :-
  258	ground(S), ground(L), member(S, L), delete(L, S, N), nal_reduce(ext_intersection(N), P), nal_f_pnn(T1, T2, T).
  259inference([inheritance(M, S), T1], [inheritance(M, int_intersection(L)), T2], [inheritance(M, P), T]) :-
  260	ground(S), ground(L), member(S, L), delete(L, S, N), nal_reduce(int_intersection(N), P), nal_f_npp(T1, T2, T).
  261inference([inheritance(M, S), T1], [inheritance(M, ext_difference(S, P)), T2], [inheritance(M, P), T]) :-
  262	atom(S), atom(P), nal_f_pnp(T1, T2, T).
  263inference([inheritance(M, S), T1], [inheritance(M, ext_difference(P, S)), T2], [inheritance(M, P), T]) :-
  264	atom(S), atom(P), nal_f_nnn(T1, T2, T).
  268inference([implication(M, P), T1], [implication(S, M), T2], [implication(S, P), T]) :-
  269	S \= P, nal_f_ded(T1, T2, T).
  270inference([implication(P, M), T1], [implication(S, M), T2], [implication(S, P), T]) :-
  271	S \= P, nal_f_abd(T1, T2, T).
  272inference([implication(M, P), T1], [implication(M, S), T2], [implication(S, P), T]) :-
  273	S \= P, nal_f_ind(T1, T2, T).
  274inference([implication(P, M), T1], [implication(M, S), T2], [implication(S, P), T]) :-
  275	S \= P, nal_f_exe(T1, T2, T).
  279inference([implication(S, P), T1], [implication(P, S), T2], [equivalence(S, P), T]) :-
  280	nal_f_int(T1, T2, T).
  284inference([implication(P, M), T1], [implication(S, M), T2], [equivalence(S, P), T]) :-
  285	S \= P, nal_f_com(T1, T2, T).
  286inference([implication(M, P), T1], [implication(M, S), T2], [equivalence(S, P), T]) :-
  287	S \= P, nal_f_com(T1, T2, T).
  288inference([implication(M, P), T1], [equivalence(S, M), T2], [implication(S, P), T]) :-
  289	S \= P, nal_f_ana(T1, T2, T).
  290inference([implication(P, M), T1], [equivalence(S, M), T2], [implication(P, S), T]) :-
  291	S \= P, nal_f_ana(T1, T2, T).
  292inference([equivalence(M, P), T1], [equivalence(S, M), T2], [equivalence(S, P), T]) :-
  293	S \= P, nal_f_res(T1, T2, T).
  297inference([implication(P, M), T1], [implication(S, M), T2], [implication(N, M), T]) :-
  298	S \= P, nal_reduce(disjunction([P, S]), N), nal_f_int(T1, T2, T).
  299inference([implication(P, M), T1], [implication(S, M), T2], [implication(N, M), T]) :-
  300	S \= P, nal_reduce(conjunction([P, S]), N), nal_f_uni(T1, T2, T).
  301inference([implication(M, P), T1], [implication(M, S), T2], [implication(M, N), T]) :-
  302	S \= P, nal_reduce(conjunction([P, S]), N), nal_f_int(T1, T2, T).
  303inference([implication(M, P), T1], [implication(M, S), T2], [implication(M, N), T]) :-
  304	S \= P, nal_reduce(disjunction([P, S]), N), nal_f_uni(T1, T2, T).
  308inference([implication(S, M), T1], [implication(disjunction(L), M), T2], [implication(P, M), T]) :-
  309	ground(S), ground(L), member(S, L), delete(L, S, N), nal_reduce(disjunction(N), P), nal_f_pnn(T1, T2, T).
  310inference([implication(S, M), T1], [implication(conjunction(L), M), T2], [implication(P, M), T]) :-
  311	ground(S), ground(L), member(S, L), delete(L, S, N), nal_reduce(conjunction(N), P), nal_f_npp(T1, T2, T).
  312inference([implication(M, S), T1], [implication(M, conjunction(L)), T2], [implication(M, P), T]) :-
  313	ground(S), ground(L), member(S, L), delete(L, S, N), nal_reduce(conjunction(N), P), nal_f_pnn(T1, T2, T).
  314inference([implication(M, S), T1], [implication(M, disjunction(L)), T2], [implication(M, P), T]) :-
  315	ground(S), ground(L), member(S, L), delete(L, S, N), nal_reduce(disjunction(N), P), nal_f_npp(T1, T2, T).
  319inference([implication(M, P), T1], [M, T2], [P, T]) :-
  320	ground(P), nal_f_ded(T1, T2, T).
  321inference([implication(P, M), T1], [M, T2], [P, T]) :-
  322	ground(P), nal_f_abd(T1, T2, T).
  323inference([M, T1], [equivalence(S, M), T2], [S, T]) :-
  324	ground(S), nal_f_ana(T1, T2, T).
  328inference([P, T1], [S, T2], [C, T]) :-
  329	C == implication(S, P), nal_f_ind(T1, T2, T).
  330inference([P, T1], [S, T2], [C, T]) :-
  331	C == equivalence(S, P), nal_f_com(T1, T2, T).
  332inference([P, T1], [S, T2], [C, T]) :-
  333	nal_reduce(conjunction([P, S]), N), N == C, nal_f_int(T1, T2, T).
  334inference([P, T1], [S, T2], [C, T]) :-
  335	nal_reduce(disjunction([P, S]), N), N == C, nal_f_uni(T1, T2, T).
  339inference([S, T1], [conjunction(L), T2], [P, T]) :-
  340	ground(S), ground(L), member(S, L), delete(L, S, N), nal_reduce(conjunction(N), P), nal_f_pnn(T1, T2, T).
  341inference([S, T1], [disjunction(L), T2], [P, T]) :-
  342	ground(S), ground(L), member(S, L), delete(L, S, N), nal_reduce(disjunction(N), P), nal_f_npp(T1, T2, T).
  346inference([implication(conjunction(L), C), T1], [M, T2], [implication(P, C), T]) :-
  347	nonvar(L), member(M, L), subtract(L, [M], A), A \= [], nal_reduce(conjunction(A), P), nal_f_ded(T1, T2, T).
  348inference([implication(conjunction(L), C), T1], [implication(P, C), T2], [M, T]) :-
  349	ground(L), member(M, L), subtract(L, [M], A), A \= [], nal_reduce(conjunction(A), P), nal_f_abd(T1, T2, T).
  350inference([implication(conjunction(L), C), T1], [M, T2], [S, T]) :-
  351	S == implication(conjunction([M|L]), C), nal_f_ind(T1, T2, T).
  352
  353inference([implication(conjunction(Lm), C), T1], [implication(A, M), T2], [implication(P, C), T]) :-
  354	nonvar(Lm), nal_replace(Lm, M, La, A), nal_reduce(conjunction(La), P), nal_f_ded(T1, T2, T).
  355inference([implication(conjunction(Lm), C), T1], [implication(conjunction(La), C), T2], [implication(A, M), T]) :-
  356	nonvar(Lm), nal_replace(Lm, M, La, A), nal_f_abd(T1, T2, T).
  357inference([implication(conjunction(La), C), T1], [implication(A, M), T2], [implication(P, C), T]) :-
  358	nonvar(La), nal_replace(Lm, M, La, A), nal_reduce(conjunction(Lm), P), nal_f_ind(T1, T2, T).
  362inference([inheritance(M, P), T1], [inheritance(M, S), T2], [implication(inheritance(X, S), inheritance(X, P)), T]) :-
  363	S \= P, nal_f_ind(T1, T2, T).
  364inference([inheritance(P, M), T1], [inheritance(S, M), T2], [implication(inheritance(P, X), inheritance(S, X)), T]) :-
  365	S \= P, nal_f_abd(T1, T2, T).
  366inference([inheritance(M, P), T1], [inheritance(M, S), T2], [equivalence(inheritance(X, S), inheritance(X, P)), T]) :-
  367	S \= P, nal_f_com(T1, T2, T).
  368inference([inheritance(P, M), T1], [inheritance(S, M), T2], [equivalence(inheritance(P, X), inheritance(S, X)), T]) :-
  369	S \= P, nal_f_com(T1, T2, T).
  370inference([inheritance(M, P), T1], [inheritance(M, S), T2], [conjunction([inheritance(var(Y, []), S), inheritance(var(Y, []), P)]), T]) :-
  371	S \= P, nal_f_int(T1, T2, T).
  372inference([inheritance(P, M), T1], [inheritance(S, M), T2], [conjunction([inheritance(S, var(Y, [])), inheritance(P, var(Y, []))]), T]) :-
  373	S \= P, nal_f_int(T1, T2, T).
  377inference([implication(A, inheritance(M1, P)), T1], [inheritance(M2, S), T2], [implication(conjunction([A, inheritance(X, S)]), inheritance(X, P)), T]) :-
  378	S \= P, M1 == M2, A \= inheritance(M2, S), nal_f_ind(T1, T2, T).
  379inference([implication(A, inheritance(M1, P)), T1], [inheritance(M2, S), T2], [conjunction([implication(A, inheritance(var(Y, []), P)), inheritance(var(Y, []), S)]), T]) :-
  380	S \= P, M1 == M2, A \= inheritance(M2, S), nal_f_int(T1, T2, T).
  381inference([conjunction(L1), T1], [inheritance(M, S), T2], [implication(inheritance(Y, S), conjunction([inheritance(Y, P2)|L3])), T]) :-
  382	subtract(L1, [inheritance(M, P)], L2), L1 \= L2, S \= P, dependent(P, Y, P2), dependent(L2, Y, L3), nal_f_ind(T1, T2, T).
  383inference([conjunction(L1), T1], [inheritance(M, S), T2], [conjunction([inheritance(var(Y, []), S), inheritance(var(Y, []), P)|L2]), T]) :-
  384	subtract(L1, [inheritance(M, P)], L2), L1 \= L2, S \= P, nal_f_int(T1, T2, T).
  385
  386inference([implication(A, inheritance(P, M1)), T1], [inheritance(S, M2), T2], [implication(conjunction([A, inheritance(P, X)]), inheritance(S, X)), T]) :-
  387	S \= P, M1 == M2, A \= inheritance(S, M2), nal_f_abd(T1, T2, T).
  388inference([implication(A, inheritance(P, M1)), T1], [inheritance(S, M2), T2], [conjunction([implication(A, inheritance(P, var(Y, []))), inheritance(S, var(Y, []))]), T]) :-
  389	S \= P, M1 == M2, A \= inheritance(S, M2), nal_f_int(T1, T2, T).
  390inference([conjunction(L1), T1], [inheritance(S, M), T2], [implication(inheritance(S, Y), conjunction([inheritance(P2, Y)|L3])), T]) :-
  391	subtract(L1, [inheritance(P, M)], L2), L1 \= L2, S \= P, dependent(P, Y, P2), dependent(L2, Y, L3), nal_f_abd(T1, T2, T).
  392inference([conjunction(L1), T1], [inheritance(S, M), T2], [conjunction([inheritance(S, var(Y, [])), inheritance(P, var(Y, []))|L2]), T]) :-
  393	subtract(L1, [inheritance(P, M)], L2), L1 \= L2, S \= P, nal_f_int(T1, T2, T).
  397inference([conjunction(L1), T1], [inheritance(M, S), T2], [C, T]) :-
  398	subtract(L1, [inheritance(var(N, D), S)], L2), L1 \= L2,
  399	replace_var(L2, var(N, D), L3, M), nal_reduce(conjunction(L3), C), nal_f_cnv(T2, T0), nal_f_ana(T1, T0, T).
  400inference([conjunction(L1), T1], [inheritance(S, M), T2], [C, T]) :-
  401	subtract(L1, [inheritance(S, var(N, D))], L2), L1 \= L2,
  402	replace_var(L2, var(N, D), L3, M), nal_reduce(conjunction(L3), C), nal_f_cnv(T2, T0), nal_f_ana(T1, T0, T).
  403
  404replace_var([], _, [], _).
  405replace_var([inheritance(S1, P)|T1], S1, [inheritance(S2, P)|T2], S2) :-
  406	replace_var(T1, S1, T2, S2).
  407replace_var([inheritance(S, P1)|T1], P1, [inheritance(S, P2)|T2], P2) :-
  408	replace_var(T1, P1, T2, P2).
  409replace_all([H|T1], H1, [H|T2], H2) :-
  410	replace_var(T1, H1, T2, H2).
  411
  412
  413
  414%%% Theorems in IL:
  415
  416% inheritance
  417
  418inheritance(ext_intersection(Ls), P) :-
  419	nal_include([P], Ls).
  420inheritance(S, int_intersection(Lp)) :-
  421	nal_include([S], Lp).
  422inheritance(ext_intersection(S), ext_intersection(P)) :-
  423	nal_include(P, S), P \= [_].
  424inheritance(int_intersection(S), int_intersection(P)) :-
  425	nal_include(S, P), S \= [_].
  426inheritance(ext_set(S), ext_set(P)) :-
  427	nal_include(S, P).
  428inheritance(int_set(S), int_set(P)) :-
  429	nal_include(P, S).
  430
  431inheritance(ext_difference(S, P), S) :-
  432	ground(S), ground(P).
  433inheritance(S, int_difference(S, P)) :-
  434	ground(S), ground(P).
  435
  436inheritance(product(L1), R) :-
  437	ground(L1), member(ext_image(R, L2), L1), nal_replace(L1, ext_image(R, L2), L2).
  438inheritance(R, product(L1)) :-
  439	ground(L1), member(int_image(R, L2), L1), nal_replace(L1, int_image(R, L2), L2).
  440
  441% similarity
  442
  443similarity(X, Y) :-
  444	ground(X), nal_reduce(X, Y), X \== Y, !.
  445
  446similarity(ext_intersection(L1), ext_intersection(L2)) :-
  447	same_set(L1, L2).
  448similarity(int_intersection(L1), int_intersection(L2)) :-
  449	same_set(L1, L2).
  450similarity(ext_set(L1), ext_set(L2)) :-
  451	same_set(L1, L2).
  452similarity(int_set(L1), int_set(L2)) :-
  453	same_set(L1, L2).
  454
  455% implication
  456
  457implication(similarity(S, P), inheritance(S, P)).
  458implication(equivalence(S, P), implication(S, P)).
  459
  460implication(conjunction(L), M) :-
  461	ground(L), member(M, L).
  462implication(M, disjunction(L)) :-
  463	ground(L), member(M, L).
  464
  465implication(conjunction(L1), conjunction(L2)) :-
  466	ground(L1), ground(L2), subset(L2, L1).
  467implication(disjunction(L1), disjunction(L2)) :-
  468	ground(L1), ground(L2), subset(L1, L2).
  469
  470implication(inheritance(S, P), inheritance(ext_intersection(Ls), ext_intersection(Lp))):-
  471	ground(Ls), ground(Lp), nal_replace(Ls, S, L, P), nal_same(L, Lp).
  472implication(inheritance(S, P), inheritance(int_intersection(Ls), int_intersection(Lp))):-
  473	ground(Ls), ground(Lp), nal_replace(Ls, S, L, P), nal_same(L, Lp).
  474implication(similarity(S, P), similarity(ext_intersection(Ls), ext_intersection(Lp))):-
  475	ground(Ls), ground(Lp), nal_replace(Ls, S, L, P), nal_same(L, Lp).
  476implication(similarity(S, P), similarity(int_intersection(Ls), int_intersection(Lp))):-
  477	ground(Ls), ground(Lp), nal_replace(Ls, S, L, P), nal_same(L, Lp).
  478
  479implication(inheritance(S, P), inheritance(ext_difference(S, M), ext_difference(P, M))):-
  480	ground(M).
  481implication(inheritance(S, P), inheritance(int_difference(S, M), int_difference(P, M))):-
  482	ground(M).
  483implication(similarity(S, P), similarity(ext_difference(S, M), ext_difference(P, M))):-
  484	ground(M).
  485implication(similarity(S, P), similarity(int_difference(S, M), int_difference(P, M))):-
  486	ground(M).
  487implication(inheritance(S, P), inheritance(ext_difference(M, P), ext_difference(M, S))):-
  488	ground(M).
  489implication(inheritance(S, P), inheritance(int_difference(M, P), int_difference(M, S))):-
  490	ground(M).
  491implication(similarity(S, P), similarity(ext_difference(M, P), ext_difference(M, S))):-
  492	ground(M).
  493implication(similarity(S, P), similarity(int_difference(M, P), int_difference(M, S))):-
  494	ground(M).
  495
  496implication(inheritance(S, P), negation(inheritance(S, ext_difference(M, P)))) :-
  497	ground(M).
  498implication(inheritance(S, ext_difference(M, P)), negation(inheritance(S, P))) :-
  499	ground(M).
  500implication(inheritance(S, P), negation(inheritance(int_difference(M, S), P))) :-
  501	ground(M).
  502implication(inheritance(int_difference(M, S), P), negation(inheritance(S, P))) :-
  503	ground(M).
  504
  505implication(inheritance(S, P), inheritance(ext_image(S, M), ext_image(P, M))) :-
  506	ground(M).
  507implication(inheritance(S, P), inheritance(int_image(S, M), int_image(P, M))) :-
  508	ground(M).
  509implication(inheritance(S, P), inheritance(ext_image(M, Lp), ext_image(M, Ls))) :-
  510	ground(Ls), ground(Lp), append(L1, [S|L2], Ls), append(L1, [P|L2], Lp).
  511implication(inheritance(S, P), inheritance(int_image(M, Lp), int_image(M, Ls))) :-
  512	ground(Ls), ground(Lp), append(L1, [S|L2], Ls), append(L1, [P|L2], Lp).
  513
  514implication(negation(M), negation(conjunction(L))) :-
  515	nal_include([M], L).
  516implication(negation(disjunction(L)), negation(M)) :-
  517	nal_include([M], L).
  518
  519implication(implication(S, P), implication(conjunction(Ls), conjunction(Lp))):-
  520	ground(Ls), ground(Lp), nal_replace(Ls, S, L, P), nal_same(L, Lp).
  521implication(implication(S, P), implication(disjunction(Ls), disjunction(Lp))):-
  522	ground(Ls), ground(Lp), nal_replace(Ls, S, L, P), nal_same(L, Lp).
  523implication(equivalence(S, P), equivalence(conjunction(Ls), conjunction(Lp))):-
  524	ground(Ls), ground(Lp), nal_replace(Ls, S, L, P), nal_same(L, Lp).
  525implication(equivalence(S, P), equivalence(disjunction(Ls), disjunction(Lp))):-
  526	ground(Ls), ground(Lp), nal_replace(Ls, S, L, P), nal_same(L, Lp).
  527
  528
  529% equivalence
  530
  531equivalence(X, Y) :-
  532	ground(X), nal_reduce(X, Y), X \== Y, !.
  533
  534equivalence(similarity(S, P), similarity(P, S)).
  535
  536equivalence(inheritance(S, ext_set([P])), similarity(S, ext_set([P]))).
  537equivalence(inheritance(int_set([S]), P), similarity(int_set([S]), P)).
  538
  539equivalence(inheritance(S, ext_intersection(Lp)), conjunction(L)) :-
  540	findall(inheritance(S, P), member(P, Lp), L).
  541equivalence(inheritance(int_intersection(Ls), P), conjunction(L)) :-
  542	findall(inheritance(S, P), member(S, Ls), L).
  543
  544equivalence(inheritance(S, ext_difference(P1, P2)),
  545	    conjunction([inheritance(S, P1), negation(inheritance(S, P2))])).
  546equivalence(inheritance(int_difference(S1, S2), P),
  547	    conjunction([inheritance(S1, P), negation(inheritance(S2, P))])).
  548
  549equivalence(inheritance(product(Ls), product(Lp)), conjunction(L)) :-
  550	equ_product(Ls, Lp, L).
  551
  552equivalence(inheritance(product([S|L]), product([P|L])), inheritance(S, P)) :-
  553	ground(L).
  554equivalence(inheritance(S, P), inheritance(product([H|Ls]), product([H|Lp]))) :-
  555	ground(H), equivalence(inheritance(product(Ls), product(Lp)), inheritance(S, P)).
  556
  557equivalence(inheritance(product(L), R), inheritance(T, ext_image(R, L1))) :-
  558	nal_replace(L, T, L1).
  559equivalence(inheritance(R, product(L)), inheritance(int_image(R, L1), T)) :-
  560	nal_replace(L, T, L1).
  561
  562equivalence(equivalence(S, P), equivalence(P, S)).
  563
  564equivalence(equivalence(negation(S), P), equivalence(negation(P), S)).
  565
  566equivalence(conjunction(L1), conjunction(L2)) :-
  567	same_set(L1, L2).
  568equivalence(disjunction(L1), disjunction(L2)) :-
  569	same_set(L1, L2).
  570
  571equivalence(implication(S, conjunction(Lp)), conjunction(L)) :-
  572	findall(implication(S, P), member(P, Lp), L).
  573equivalence(implication(disjunction(Ls), P), conjunction(L)) :-
  574	findall(implication(S, P), member(S, Ls), L).
  575
  576equivalence(T1, T2) :-
  577	not(atom(T1)), not(atom(T2)), ground(T1), ground(T2),
  578	T1 =.. L1, T2 =.. L2, equivalence_list(L1, L2).
  579
  580equivalence_list(L, L).
  581equivalence_list([H|L1], [H|L2]) :-
  582	equivalence_list(L1, L2).
  583equivalence_list([H1|L1], [H2|L2]) :-
  584	similarity(H1, H2), equivalence_list(L1, L2).
  585equivalence_list([H1|L1], [H2|L2]) :-
  586	equivalence(H1, H2), equivalence_list(L1, L2).
  587
  588% compound term structure reduction
  589
  590nal_reduce(similarity(ext_set([S]), ext_set([P])), similarity(S, P)) :-
  591	!.
  592nal_reduce(similarity(int_set([S]), int_set([P])), similarity(S, P)) :-
  593	!.
  594
  595nal_reduce(instance(S, P), inheritance(ext_set([S]), P)) :-
  596	!.
  597nal_reduce(property(S, P), inheritance(S, int_set([P]))) :-
  598	!.
  599nal_reduce(inst_prop(S, P), inheritance(ext_set([S]), int_set([P]))) :-
  600	!.
  601
  602nal_reduce(ext_intersection([T]), T) :-
  603	!.
  604nal_reduce(int_intersection([T]), T) :-
  605	!.
  606
  607nal_reduce(ext_intersection([ext_intersection(L1), ext_intersection(L2)]), ext_intersection(L)) :-
  608	union(L1, L2, L), !.
  609nal_reduce(ext_intersection([ext_intersection(L1), L2]), ext_intersection(L)) :-
  610	union(L1, [L2], L), !.
  611nal_reduce(ext_intersection([L1, ext_intersection(L2)]), ext_intersection(L)) :-
  612	union([L1], L2, L), !.
  613nal_reduce(ext_intersection([ext_set(L1), ext_set(L2)]), ext_set(L)) :-
  614	intersection(L1, L2, L), !.
  615nal_reduce(ext_intersection([int_set(L1), int_set(L2)]), int_set(L)) :-
  616	union(L1, L2, L), !.
  617
  618nal_reduce(int_intersection([int_intersection(L1), int_intersection(L2)]), int_intersection(L)) :-
  619	union(L1, L2, L), !.
  620nal_reduce(int_intersection([int_intersection(L1), L2]), int_intersection(L)) :-
  621	union(L1, [L2], L), !.
  622nal_reduce(int_intersection([L1, int_intersection(L2)]), int_intersection(L)) :-
  623	union([L1], L2, L), !.
  624nal_reduce(int_intersection([int_set(L1), int_set(L2)]), int_set(L)) :-
  625	intersection(L1, L2, L), !.
  626nal_reduce(int_intersection([ext_set(L1), ext_set(L2)]), ext_set(L)) :-
  627	union(L1, L2, L), !.
  628
  629nal_reduce(ext_difference(ext_set(L1), ext_set(L2)), ext_set(L)) :-
  630	subtract(L1, L2, L), !.
  631nal_reduce(int_difference(int_set(L1), int_set(L2)), int_set(L)) :-
  632	subtract(L1, L2, L), !.
  633
  634nal_reduce(product(product(L), T), product(L1)) :-
  635	append(L, [T], L1), !.
  636
  637nal_reduce(ext_image(product(L1), L2), T1) :-
  638	member(T1, L1), nal_replace(L1, T1, L2), !.
  639nal_reduce(int_image(product(L1), L2), T1) :-
  640	member(T1, L1), nal_replace(L1, T1, L2), !.
  641
  642nal_reduce(negation(negation(S)), S) :-
  643	!.
  644
  645nal_reduce(conjunction([T]), T) :-
  646	!.
  647nal_reduce(disjunction([T]), T) :-
  648	!.
  649
  650nal_reduce(conjunction([conjunction(L1), conjunction(L2)]), conjunction(L)) :-
  651	union(L1, L2, L), !.
  652nal_reduce(conjunction([conjunction(L1), L2]), conjunction(L)) :-
  653	union(L1, [L2], L), !.
  654nal_reduce(conjunction([L1, conjunction(L2)]), conjunction(L)) :-
  655	union([L1], L2, L), !.
  656
  657nal_reduce(disjunction(disjunction(L1), disjunction(L2)), disjunction(L)) :-
  658	union(L1, L2, L), !.
  659nal_reduce(disjunction(disjunction(L1), L2), disjunction(L)) :-
  660	union(L1, [L2], L), !.
  661nal_reduce(disjunction(L1, disjunction(L2)), disjunction(L)) :-
  662	union([L1], L2, L), !.
  663
  664nal_reduce(X, X).
  665
  666
  667%%% Argument processing
  668
  669equ_product([], [], []).
  670equ_product([T|Ls], [T|Lp], L) :-
  671	equ_product(Ls, Lp, L), !.
  672equ_product([S|Ls], [P|Lp], [inheritance(S, P)|L]) :-
  673	equ_product(Ls, Lp, L).
  674
  675same_set(L1, L2) :-
  676	L1 \== [], L1 \== [_], nal_same(L1, L2), L1 \== L2.
  677
  678nal_same([], []).
  679nal_same(L, [H|T]) :-
  680	member(H, L), subtract(L, [H], L1), nal_same(L1, T).
  681
  682nal_include(L1, L2) :-
  683	ground(L2), include1(L1, L2), L1 \== [], L1 \== L2.
  684
  685include1([], _).
  686include1([H|T1], [H|T2]) :-
  687	include1(T1, T2).
  688include1([H1|T1], [H2|T2]) :-
  689	H2 \== H1, include1([H1|T1], T2).
  690
  691nal_not_member(_, []).
  692nal_not_member(C, [C|_]) :- !, fail.
  693nal_not_member([S, T], [[S1, T]|_]) :- equivalence(S, S1), !, fail.
  694nal_not_member(C, [_|L]) :- nal_not_member(C, L).
  695
  696nal_replace([T|L], T, [nil|L]).
  697nal_replace([H|L], T, [H|L1]) :-
  698	nal_replace(L, T, L1).
  699
  700nal_replace([H1|T], H1, [H2|T], H2).
  701nal_replace([H|T1], H1, [H|T2], H2) :-
  702	nal_replace(T1, H1, T2, H2).
  703
  704dependent(var(V, L), Y, var(V, [Y|L])) :-
  705	!.
  706dependent([H|T], Y, [H1|T1]) :-
  707	dependent(H, Y, H1), dependent(T, Y, T1), !.
  708dependent(inheritance(S, P), Y, inheritance(S1, P1)) :-
  709	dependent(S, Y, S1), dependent(P, Y, P1), !.
  710dependent(ext_image(R, A), Y, ext_image(R, A1)) :-
  711	dependent(A, Y, A1), !.
  712dependent(int_image(R, A), Y, int_image(R, A1)) :-
  713	dependent(A, Y, A1), !.
  714dependent(X, _, X).
  715
  716
  717%%% Truth-value functions
  718
  719nal_f_rev([F1, C1], [F2, C2], [F, C]) :-
  720     C1 < 1,
  721     C2 < 1,
  722	M1 is C1 / (1 - C1),
  723	M2 is C2 / (1 - C2),
  724	F is (M1 * F1 + M2 * F2) / (M1 + M2),
  725	C is (M1 + M2) / (M1 + M2 + 1).
  726
  727nal_f_exp([F, C], E) :-
  728	E is C * (F - 0.5) + 0.5.
  729
  730nal_f_neg([F1, C1], [F, C1]) :-
  731	u_not(F1, F).
  732
  733nal_f_cnv([F1, C1], [1, C]) :-
  734     u_and([F1, C1], W),
  735	u_w2c(W, C).
  736
  737nal_f_cnt([F1, C1], [0, C]) :-
  738	u_not(F1, F0),
  739     u_and([F0, C1], W),
  740	u_w2c(W, C).
  741
  742nal_f_ded([F1, C1], [F2, C2], [F, C]) :-
  743	u_and([F1, F2], F),
  744	u_and([C1, C2, F], C).
  745
  746nal_f_ana([F1, C1], [F2, C2], [F, C]) :-
  747	u_and([F1, F2], F),
  748	u_and([C1, C2, F2], C).
  749
  750nal_f_res([F1, C1], [F2, C2], [F, C]) :-
  751	u_and([F1, F2], F),
  752	u_or([F1, F2], F0),
  753	u_and([C1, C2, F0], C).
  754
  755nal_f_abd([F1, C1], [F2, C2], [F2, C]) :-
  756	u_and([F1, C1, C2], W),
  757	u_w2c(W, C).
  758
  759nal_f_ind(T1, T2, T) :-
  760	nal_f_abd(T2, T1, T).
  761
  762nal_f_exe([F1, C1], [F2, C2], [1, C]) :-
  763	u_and([F1, C1, F2, C2], W),
  764	u_w2c(W, C).
  765
  766nal_f_com([0, _C1], [0, _C2], [0, 0]).
  767nal_f_com([F1, C1], [F2, C2], [F, C]) :-
  768	u_or([F1, F2], F0),
  769	F0 > 0,
  770	F is F1 * F2 / F0,
  771	u_and([F0, C1, C2], W),
  772	u_w2c(W, C).
  773
  774nal_f_int([F1, C1], [F2, C2], [F, C]) :-
  775	u_and([F1, F2], F),
  776	u_and([C1, C2], C).
  777
  778nal_f_uni([F1, C1], [F2, C2], [F, C]) :-
  779	u_or([F1, F2], F),
  780	u_and([C1, C2], C).
  781
  782nal_f_dif([F1, C1], [F2, C2], [F, C]) :-
  783	u_not(F2, F0),
  784	u_and([F1, F0], F),
  785	u_and([C1, C2], C).
  786
  787nal_f_pnn([F1, C1], [F2, C2], [F, C]) :-
  788	u_not(F2, F2n),
  789	u_and([F1, F2n], Fn),
  790	u_not(Fn, F),
  791	u_and([Fn, C1, C2], C).
  792
  793nal_f_npp([F1, C1], [F2, C2], [F, C]) :-
  794	u_not(F1, F1n),
  795	u_and([F1n, F2], F),
  796	u_and([F, C1, C2], C).
  797
  798nal_f_pnp([F1, C1], [F2, C2], [F, C]) :-
  799	u_not(F2, F2n),
  800	u_and([F1, F2n], F),
  801	u_and([F, C1, C2], C).
  802
  803nal_f_nnn([F1, C1], [F2, C2], [F, C]) :-
  804	u_not(F1, F1n),
  805	u_not(F2, F2n),
  806	u_and([F1n, F2n], Fn),
  807	u_not(Fn, F),
  808	u_and([Fn, C1, C2], C).
  809
  810% Utility functions
  811
  812u_not(N0, N) :-
  813	N is (1 - N0), !.
  814
  815u_and([N], N).
  816u_and([N0 | Nt], N) :-
  817	u_and(Nt, N1), N is N0 * N1, !.
  818
  819u_or([N], N).
  820u_or([N0 | Nt], N) :-
  821	u_or(Nt, N1), N is (N0 + N1 - N0 * N1), !.
  822
  823u_w2c(W, C) :-
  824	K = 1, C is (W / (W + K)), !.
  825
  826:- fixup_exports.  827
  828
  829/*
  830User's Guide of NAL
  831Input/Output Language
  832In this demonstration, NAL implements the following formal language, Narsese. The input and output of the system are Narsese judgments.
  833           <judgment> ::= [<statement> [frequency-value, confidence-value]]
  834          <statement> ::= <relation>(<term>, <term>)
  835                        | <compound-statement>
  836                        | <term>
  837               <term> ::= <word>
  838                        | <variable>
  839                        | <compound-term>
  840                        | <statement>
  841           <variable> ::= <independent-variable>
  842                        | <dependent-variable>(<independent-variable>*)
  843           <relation> ::= inheritance
  844                        | similarity
  845                        | implication
  846                        | equivalence
  847                        | instance
  848                        | property
  849                        | inst_prop                                // instance-property
  850 <compound-statement> ::= negation(<statement>)
  851                        | conjunction([<statement>, <statement>+])
  852                        | disjunction([<statement>, <statement>+])
  853      <compound-term> ::= ext_set([<term>+])                       // extensional set
  854                        | int_set([<term>+])                       // intensional set
  855                        | ext_intersection([<term>, <term>+])      // extensional intersection
  856                        | int_intersection([<term>, <term>+])      // intensional intersection
  857                        | ext_difference(<term>, <term>)           // extensional difference
  858                        | int_difference(<term>, <term>)           // intensional difference
  859                        | product([<term>, <term>+])
  860                        | ext_image(<term>, <term>)                // extensional image
  861                        | int_image(<term>, <term>)                // intensional image
  862The frequency-value is a real number in [0, 1]; the confidence-value a real number in (0, 1).
  863User Interface
  864The program can be invoked in the following ways:
  865revision(J1, J2, J).
  866Judgment J is the result of a revision between judgments J1 and J2. The three judgments all have the nal_same statement in them.
  867choice(J1, J2, J).
  868Judgment J is the result of a choice between judgments J1 and J2.
  869inference(J1, J2, J).
  870Judgment J is the conclusion derived from judgments J1 and J2 as premises.
  871inference(J1, J).
  872Judgment J is the conclusion derived from judgment J1 as single premise.
  873
  874*/