1% nal.pl
    2% Non-Axiomatic Logic in Prolog
    3% Version: 1.1, September 2012
    4% GNU Lesser General Public License
    5% Author: Pei Wang/Pat Hammer/Douglas Miles
    6
    7:- module(nars, [nars_main/1,nars_main/0]).    8
    9:- set_module(class(library)).   10:- set_module(base(system)).   11
   12:- use_module(library(nars/nal_reader)). 
   13
   14% will change later to what we consider "enough" ground
   15narz_ground(G):-  ground(G).
   16
   17nars_string(Name):- atom(Name) ; string(Name).
   18
   19do_nars_example_tests:- 
   20  use_module(library('nars/../../examples/prolog/nal_examples'),[nal_example_test/2]),
   21  add_history(run_nars_example_tests),
   22  run_nars_example_tests.
   23
   24run_nars_example_tests:-
   25  forall(nal_examples:nal_example_test(Goal, Results),
   26         do_nars_example_test(Goal, Results)).
   27
   28baseKB:sanity_test:- do_nars_example_tests.
   29
   30baseKB:feature_test:- run_nars_example_tests.
   31/*
   32```diff
   33- text in red
   34+ text in green
   35! text in orange
   36# text in gray
   37@@ text in purple (and bold)@@
   38```
   39*/
   40do_nars_example_test(Goal, ResultsExpected):-   
   41  format('~N~n```prolog~nTEST: ?- ~q.~n```',[Goal]),
   42  % term_variables(Goal,Vs),
   43  maplist([R]>>format('~NEXPECTED: `~q`',[R]), ResultsExpected),
   44  ((call(Goal),narz_check_results(ResultsExpected))
   45    -> format('~N~n```diff~n+SUCCESS!~n```',[])
   46     ; format('~N~n```diff~n-FAILED!~n```',[])
   47     ), !,
   48  format('~n~n```prolog',[]),
   49  mu:dbug1(ResultsExpected),
   50  format('```~n~n',[]).
   51
   52narz_check_results([R1;R2]):- !, narz_check_results(R1) ; narz_check_results(R2).
   53narz_check_results([R1|RS]):- !, narz_check_results(R1), !, narz_check_results(RS).
   54narz_check_results([]):-!.
   55narz_check_results(R):- call(R),!.
   56narz_check_results(R=V):- nars_close_enough(R,V).
   57
   58nars_close_enough(R,V):- number(R),number(V),!, RV is abs(R-V), RV < 0.02 .
   59nars_close_enough(R,V):- (\+ compound(R) ; \+ compound(V)),!, R==V, !.
   60nars_close_enough([R|RT],[V|VT]):- !, nars_close_enough(R,V),nars_close_enough(RT,VT).
   61nars_close_enough(R,V):- 
   62  compound_name_arguments(R,F,RA),
   63  compound_name_arguments(V,F,VA),
   64  maplist(nars_close_enough,RA,VA).
   65
   66%like to distinguish "eaten by tiger" from "eating tiger" (/, eat, tiger, _) vs. (/, eat, _, tiger)
   67%now: (eat /2 tiger) vs. (eat /1 tiger)
   68
   69use_nars_config_info(List):-  is_list(List), !, maplist(use_nars_config_info, List).
   70use_nars_config_info(element(_, [], List)):- !, use_nars_config_info(List).
   71use_nars_config_info(element(_, [name=Name, value=Value], _)):- !, use_nars_config_info(Name=Value).
   72use_nars_config_info(Name=Value):- nars_string(Name), downcase_atom(Name, NameD), NameD\=Name, !, use_nars_config_info(NameD=Value).
   73use_nars_config_info(Name=Value):- nars_string(Value), downcase_atom(Value, ValueD), ValueD\=Value, !, use_nars_config_info(Name=ValueD).
   74use_nars_config_info(Name=Value):-  atom(Value), atom_number(Value, Number), use_nars_config_info(Name=Number).
   75%use_nars_config_info(Ignore):- nars_string(Ignore), !.
   76%use_nars_config_info(NameValue):-  dmsg(use_nars_config_info(NameValue)), fail.
   77%use_nars_config_info(Name=Value):-  number(Value), !, nb_setval(Name, Value).
   78use_nars_config_info(Name=Value):-  nb_setval(Name, Value).
   79use_nars_config_info(_).
   80
   81
   82% default gobals
   83:-  use_nars_config_info(volume=100).   84:-  use_nars_config_info(novelty_horizon=100000).   85:-  use_nars_config_info(decision_threshold=0.51).   86:-  use_nars_config_info(concept_bag_size=80000).   87:-  use_nars_config_info(concept_bag_levels=1000).   88:-  use_nars_config_info(duration=5).   89:-  use_nars_config_info(horizon=1).   90:-  use_nars_config_info(truth_epsilon=0.01).   91:-  use_nars_config_info(budget_epsilon=0.0001).   92:-  use_nars_config_info(budget_threshold=0.01).   93:-  use_nars_config_info(default_confirmation_expectation=0.6).   94:-  use_nars_config_info(always_create_concept=true).   95:-  use_nars_config_info(default_creation_expectation=0.66).   96:-  use_nars_config_info(default_creation_expectation_goal=0.6).   97:-  use_nars_config_info(default_judgment_confidence=0.9).   98:-  use_nars_config_info(default_judgment_priority=0.8).   99:-  use_nars_config_info(default_judgment_durability=0.5).  100:-  use_nars_config_info(default_question_priority=0.9).  101:-  use_nars_config_info(default_question_durability=0.9).  102:-  use_nars_config_info(default_goal_confidence=0.9).  103:-  use_nars_config_info(default_goal_priority=0.9).  104:-  use_nars_config_info(default_goal_durability=0.9).  105:-  use_nars_config_info(default_quest_priority=0.9).  106:-  use_nars_config_info(default_quest_durability=0.9).  107:-  use_nars_config_info(bag_threshold=1.0).  108:-  use_nars_config_info(forget_quality_relative=0.3).  109:-  use_nars_config_info(revision_max_occurrence_distance=10).  110:-  use_nars_config_info(task_link_bag_size=100).  111:-  use_nars_config_info(task_link_bag_levels=10).  112:-  use_nars_config_info(term_link_bag_size=100).  113:-  use_nars_config_info(term_link_bag_levels=10).  114:-  use_nars_config_info(term_link_max_matched=10).  115:-  use_nars_config_info(novel_task_bag_size=1000).  116:-  use_nars_config_info(novel_task_bag_levels=100).  117:-  use_nars_config_info(novel_task_bag_selections=100).  118:-  use_nars_config_info(sequence_bag_size=30).  119:-  use_nars_config_info(sequence_bag_levels=10).  120:-  use_nars_config_info(operation_bag_size=10).  121:-  use_nars_config_info(operation_bag_levels=10).  122:-  use_nars_config_info(operation_samples=6).  123:-  use_nars_config_info(projection_decay=0.1).  124:-  use_nars_config_info(maximum_evidental_base_length=20000).  125:-  use_nars_config_info(termlink_max_reasoned=3).  126:-  use_nars_config_info(term_link_record_length=10).  127:-  use_nars_config_info(concept_beliefs_max=28).  128:-  use_nars_config_info(concept_questions_max=5).  129:-  use_nars_config_info(concept_goals_max=7).  130:-  use_nars_config_info(reliance=0.9).  131:-  use_nars_config_info(discount_rate=0.5).  132:-  use_nars_config_info(immediate_eternalization=true).  133:-  use_nars_config_info(sequence_bag_attempts=10).  134:-  use_nars_config_info(condition_bag_attempts=10).  135:-  use_nars_config_info(derivation_priority_leak=0.4).  136:-  use_nars_config_info(derivation_durability_leak=0.4).  137:-  use_nars_config_info(curiosity_desire_confidence_mul=0.1).  138:-  use_nars_config_info(curiosity_desire_priority_mul=0.1).  139:-  use_nars_config_info(curiosity_desire_durability_mul=0.3).  140:-  use_nars_config_info(curiosity_for_operator_only=false).  141:-  use_nars_config_info(break_nal_hol_boundary=false).  142:-  use_nars_config_info(question_generation_on_decision_making=false).  143:-  use_nars_config_info(how_question_generation_on_decision_making=false).  144:-  use_nars_config_info(anticipation_confidence=0.1).  145:-  use_nars_config_info(anticipation_tolerance=100.0).  146:-  use_nars_config_info(retrospective_anticipations=false).  147:-  use_nars_config_info(satisfaction_treshold=0.0).  148:-  use_nars_config_info(complexity_unit=1.0).  149:-  use_nars_config_info(interval_adapt_speed=4.0).  150:-  use_nars_config_info(tasklink_per_content=4).  151:-  use_nars_config_info(default_feedback_priority=0.9).  152:-  use_nars_config_info(default_feedback_durability=0.5).  153:-  use_nars_config_info(concept_forget_durations=2.0).  154:-  use_nars_config_info(termlink_forget_durations=10.0).  155:-  use_nars_config_info(tasklink_forget_durations=4.0).  156:-  use_nars_config_info(event_forget_durations=4.0).  157:-  use_nars_config_info(variable_introduction_combinations_max=8).  158:-  use_nars_config_info(variable_introduction_confidence_mul=0.9).  159:-  use_nars_config_info(anticipations_per_concept_max=8).  160:-  use_nars_config_info(motor_babbling_confidence_threshold=0.8).  161:-  use_nars_config_info(threads_amount=1).  162:-  use_nars_config_info(milliseconds_per_step=0).  163:-  use_nars_config_info(steps_clock=true).  164:-  use_nars_config_info(derivation_durability_leak=0.4).  165:-  use_nars_config_info(derivation_priority_leak=0.4).  166
  167use_nars_config(File):-  (\+ atom(File); \+ is_absolute_file_name(File)),
  168   absolute_file_name(File, Absolute), !, use_nars_config(Absolute).
  169use_nars_config(Absolute):-  open(Absolute, read, In),
  170    load_sgml(In, Dom,
  171                   [  dialect(html5),
  172                      attribute_value(string),
  173                      cdata(string),
  174                     nars_system_entities(true),
  175                     nars_space(remove),
  176                     nars_syntax_errors(quiet),
  177                      case_preserving_attributes(false),
  178                      case_sensitive_attributes(false),
  179                   max_errors(-1)]), !,
  180    close(In),
  181    use_nars_config_info(Dom), !.
  182
  183 parse_config:-
  184   use_nars_config(library('../config/mvpConfig.xml')).
  185
  186
  187
  188% This program covers the inferencerules of upto NAL-6 in
  189% "Non-Axiomatic Logic: A Model of Intelligent Reasoning"
  190% For the details of syntax, see the "User's Guide of NAL"
  191
  192%%% individual inferencerules
  193
  194% There are three types of inferencerules in NAL:
  195% (1) "revision" merges its two premises into a conclusion;
  196% (2) "choice"nars_selects one of its two premises as a conclusion;
  197% (3) "inference" generates a conclusion from one or two premises.
  198
  199nars_ctx(default).
  200
  201%revision/3
  202revision([S, T1], [S, T2], [S, T]):- nars_revision([S, T1], [S, T2], [S, T]).
  203
  204nars_revision([S, T1], [S, T2], [S, T]):-
  205 	narz_f_rev(T1, T2, T).
  206
  207%NARS choice/3
  208choice(X, Y, Z):- nars_choice(X, Y, Z).
  209
  210nars_choice([S, [F1, C1]], [S, [_F2, C2]], [S, [F1, C1]]):-
  211 	C1 >= C2, !.
  212nars_choice([S, [_F1, C1]], [S, [F2, C2]], [S, [F2, C2]]):-
  213 	C1 < C2, !.
  214nars_choice([S1, T1], [S2, T2], [S1, T1]):-
  215 	S1 \= S2, narz_f_exp(T1, E1), narz_f_exp(T2, E2), E1 >= E2, !.
  216nars_choice([S1, T1], [S2, T2], [S2, T2]):-
  217 	S1 \= S2, narz_f_exp(T1, E1), narz_f_exp(T2, E2), E1 < E2, !.
  218
  219
  220%NARS infer-ence/2 (simplified version)
  221infer(T1, T):- nars_infer(T1, T).
  222
  223nars_infer(T1, T):-  nars_ctx(Ctx), nars_inference(Ctx, [T1, [1, 0.9]], T).
  224
  225nars_infer(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]):-
  226   narz_f_ind([1, 0.9], [1, 0.9], V), !.
  227
  228nars_infer(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]):-
  229 narz_f_ind([1, 0.9], [1, 0.9], V), !.
  230
  231nars_infer(T1, T2, T):-  nars_ctx(Ctx), nars_inference(Ctx, [T1, [1, 0.9]], [T2, [1, 0.9]], T).
  232
  233
  234%NARS inference/2
  235inference(T1, T):- nars_ctx(Ctx), nars_inference(Ctx, T1, T).
  239nars_inference(_Ctx, [inheritance(S, P), T1], [inheritance(P, S), T]):-
  240 	narz_f_cnv(T1, T).
  241nars_inference(_Ctx, [implication(S, P), T1], [implication(P, S), T]):-
  242 	narz_f_cnv(T1, T).
  243nars_inference(_Ctx, [implication(negation(S), P), T1], [implication(negation(P), S), T]):-
  244 	narz_f_cnt(T1, T).
  245
  246nars_inference(_Ctx, [negation(S), T1], [S, T]):-
  247 	narz_f_neg(T1, T).
  248nars_inference(_Ctx, [S, [F1, C1]], [negation(S), T]):-
  249 	F1 < 0.5, narz_f_neg([F1, C1], T).
  253nars_inference(_Ctx, [S1, T], [S, T]):-
  254 	narz_reduce(S1, S), S1 \== S, !.
  255nars_inference(Ctx, [S1, T], [S, T]):-
  256 	nars_equivalence(Ctx, S1, S);nars_equivalence(Ctx, S, S1).
  257
  258nars_inference(Ctx, P, C):-
  259 	nars_inference(Ctx, P, [S, [1, 1]], C), call(S).
  260nars_inference(Ctx, P, C):-
  261 	nars_inference(Ctx, [S, [1, 1]], P, C), call(S).
  262
  263
  264% inference/3
  265inference(X, Y, Z):- nars_ctx(Ctx), nars_inference(Ctx, X, Y, Z).
  270nars_inference(_Ctx, [inheritance(M, P), T1], [inheritance(S, M), T2], [inheritance(S, P), T]):-
  271 	S \= P, narz_f_ded(T1, T2, T).
  272nars_inference(_Ctx, [inheritance(P, M), T1], [inheritance(S, M), T2], [inheritance(S, P), T]):-
  273 	S \= P, narz_f_abd(T1, T2, T).
  274nars_inference(_Ctx, [inheritance(M, P), T1], [inheritance(M, S), T2], [inheritance(S, P), T]):-
  275 	S \= P, narz_f_ind(T1, T2, T).
  276nars_inference(_Ctx, [inheritance(P, M), T1], [inheritance(M, S), T2], [inheritance(S, P), T]):-
  277 	S \= P, narz_f_exe(T1, T2, T).
  281nars_inference(_Ctx, [inheritance(S, P), T1], [inheritance(P, S), T2], [similarity(S, P), T]):-
  282 	narz_f_int(T1, T2, T).
  286nars_inference(_Ctx, [inheritance(P, M), T1], [inheritance(S, M), T2], [similarity(S, P), T]):-
  287 	S \= P, narz_f_com(T1, T2, T).
  288nars_inference(_Ctx, [inheritance(M, P), T1], [inheritance(M, S), T2], [similarity(S, P), T]):-
  289 	S \= P, narz_f_com(T1, T2, T).
  290nars_inference(_Ctx, [inheritance(M, P), T1], [similarity(S, M), T2], [inheritance(S, P), T]):-
  291 	S \= P, narz_f_ana(T1, T2, T).
  292nars_inference(_Ctx, [inheritance(P, M), T1], [similarity(S, M), T2], [inheritance(P, S), T]):-
  293 	S \= P, narz_f_ana(T1, T2, T).
  294nars_inference(_Ctx, [similarity(M, P), T1], [similarity(S, M), T2], [similarity(S, P), T]):-
  295 	S \= P, narz_f_res(T1, T2, T).
  299nars_inference(_Ctx, [inheritance(P, M), T1], [inheritance(S, M), T2], [inheritance(N, M), T]):-
  300 	S \= P, narz_reduce(int_intersection([P, S]), N), narz_f_int(T1, T2, T).
  301nars_inference(_Ctx, [inheritance(P, M), T1], [inheritance(S, M), T2], [inheritance(N, M), T]):-
  302 	S \= P, narz_reduce(ext_intersection([P, S]), N), narz_f_uni(T1, T2, T).
  303nars_inference(_Ctx, [inheritance(P, M), T1], [inheritance(S, M), T2], [inheritance(N, M), T]):-
  304 	S \= P, narz_reduce(int_difference(P, S), N), narz_f_dif(T1, T2, T).
  305nars_inference(_Ctx, [inheritance(M, P), T1], [inheritance(M, S), T2], [inheritance(M, N), T]):-
  306 	S \= P, narz_reduce(ext_intersection([P, S]), N), narz_f_int(T1, T2, T).
  307nars_inference(_Ctx, [inheritance(M, P), T1], [inheritance(M, S), T2], [inheritance(M, N), T]):-
  308 	S \= P, narz_reduce(int_intersection([P, S]), N), narz_f_uni(T1, T2, T).
  309nars_inference(_Ctx, [inheritance(M, P), T1], [inheritance(M, S), T2], [inheritance(M, N), T]):-
  310 	S \= P, narz_reduce(ext_difference(P, S), N), narz_f_dif(T1, T2, T).
  314nars_inference(_Ctx, [inheritance(S, M), T1], [inheritance(int_intersection(L), M), T2], [inheritance(P, M), T]):-
  315 	narz_ground(S), narz_ground(L), member(S, L), delete(L, S, N), narz_reduce(int_intersection(N), P), narz_f_pnn(T1, T2, T).
  316nars_inference(_Ctx, [inheritance(S, M), T1], [inheritance(ext_intersection(L), M), T2], [inheritance(P, M), T]):-
  317 	narz_ground(S), narz_ground(L), member(S, L), delete(L, S, N), narz_reduce(ext_intersection(N), P), narz_f_npp(T1, T2, T).
  318nars_inference(_Ctx, [inheritance(S, M), T1], [inheritance(int_difference(S, P), M), T2], [inheritance(P, M), T]):-
  319 	atom(S), atom(P), narz_f_pnp(T1, T2, T).
  320nars_inference(_Ctx, [inheritance(S, M), T1], [inheritance(int_difference(P, S), M), T2], [inheritance(P, M), T]):-
  321 	atom(S), atom(P), narz_f_nnn(T1, T2, T).
  322nars_inference(_Ctx, [inheritance(M, S), T1], [inheritance(M, ext_intersection(L)), T2], [inheritance(M, P), T]):-
  323 	narz_ground(S), narz_ground(L), member(S, L), delete(L, S, N), narz_reduce(ext_intersection(N), P), narz_f_pnn(T1, T2, T).
  324nars_inference(_Ctx, [inheritance(M, S), T1], [inheritance(M, int_intersection(L)), T2], [inheritance(M, P), T]):-
  325 	narz_ground(S), narz_ground(L), member(S, L), delete(L, S, N), narz_reduce(int_intersection(N), P), narz_f_npp(T1, T2, T).
  326nars_inference(_Ctx, [inheritance(M, S), T1], [inheritance(M, ext_difference(S, P)), T2], [inheritance(M, P), T]):-
  327 	atom(S), atom(P), narz_f_pnp(T1, T2, T).
  328nars_inference(_Ctx, [inheritance(M, S), T1], [inheritance(M, ext_difference(P, S)), T2], [inheritance(M, P), T]):-
  329 	atom(S), atom(P), narz_f_nnn(T1, T2, T).
  333nars_inference(_Ctx, [implication(M, P), T1], [implication(S, M), T2], [implication(S, P), T]):-
  334 	S \= P, narz_f_ded(T1, T2, T).
  335nars_inference(_Ctx, [implication(P, M), T1], [implication(S, M), T2], [implication(S, P), T]):-
  336 	S \= P, narz_f_abd(T1, T2, T).
  337nars_inference(_Ctx, [implication(M, P), T1], [implication(M, S), T2], [implication(S, P), T]):-
  338 	S \= P, narz_f_ind(T1, T2, T).
  339nars_inference(_Ctx, [implication(P, M), T1], [implication(M, S), T2], [implication(S, P), T]):-
  340 	S \= P, narz_f_exe(T1, T2, T).
  344nars_inference(_Ctx, [implication(S, P), T1], [implication(P, S), T2], [equivalence(S, P), T]):-
  345 	narz_f_int(T1, T2, T).
  349nars_inference(_Ctx, [implication(P, M), T1], [implication(S, M), T2], [equivalence(S, P), T]):-
  350 	S \= P, narz_f_com(T1, T2, T).
  351nars_inference(_Ctx, [implication(M, P), T1], [implication(M, S), T2], [equivalence(S, P), T]):-
  352 	S \= P, narz_f_com(T1, T2, T).
  353nars_inference(_Ctx, [implication(M, P), T1], [equivalence(S, M), T2], [implication(S, P), T]):-
  354 	S \= P, narz_f_ana(T1, T2, T).
  355nars_inference(_Ctx, [implication(P, M), T1], [equivalence(S, M), T2], [implication(P, S), T]):-
  356 	S \= P, narz_f_ana(T1, T2, T).
  357nars_inference(_Ctx, [equivalence(M, P), T1], [equivalence(S, M), T2], [equivalence(S, P), T]):-
  358 	S \= P, narz_f_res(T1, T2, T).
  362nars_inference(_Ctx, [implication(P, M), T1], [implication(S, M), T2], [implication(N, M), T]):-
  363 	S \= P, narz_reduce(disjunction([P, S]), N), narz_f_int(T1, T2, T).
  364nars_inference(_Ctx, [implication(P, M), T1], [implication(S, M), T2], [implication(N, M), T]):-
  365 	S \= P, narz_reduce(conjunction([P, S]), N), narz_f_uni(T1, T2, T).
  366nars_inference(_Ctx, [implication(M, P), T1], [implication(M, S), T2], [implication(M, N), T]):-
  367 	S \= P, narz_reduce(conjunction([P, S]), N), narz_f_int(T1, T2, T).
  368nars_inference(_Ctx, [implication(M, P), T1], [implication(M, S), T2], [implication(M, N), T]):-
  369 	S \= P, narz_reduce(disjunction([P, S]), N), narz_f_uni(T1, T2, T).
  373nars_inference(_Ctx, [implication(S, M), T1], [implication(disjunction(L), M), T2], [implication(P, M), T]):-
  374 	narz_ground(S), narz_ground(L), member(S, L), delete(L, S, N), narz_reduce(disjunction(N), P), narz_f_pnn(T1, T2, T).
  375nars_inference(_Ctx, [implication(S, M), T1], [implication(conjunction(L), M), T2], [implication(P, M), T]):-
  376 	narz_ground(S), narz_ground(L), member(S, L), delete(L, S, N), narz_reduce(conjunction(N), P), narz_f_npp(T1, T2, T).
  377nars_inference(_Ctx, [implication(M, S), T1], [implication(M, conjunction(L)), T2], [implication(M, P), T]):-
  378 	narz_ground(S), narz_ground(L), member(S, L), delete(L, S, N), narz_reduce(conjunction(N), P), narz_f_pnn(T1, T2, T).
  379nars_inference(_Ctx, [implication(M, S), T1], [implication(M, disjunction(L)), T2], [implication(M, P), T]):-
  380 	narz_ground(S), narz_ground(L), member(S, L), delete(L, S, N), narz_reduce(disjunction(N), P), narz_f_npp(T1, T2, T).
  384nars_inference(_Ctx, [implication(M, P), T1], [M, T2], [P, T]):-
  385 	narz_ground(P), narz_f_ded(T1, T2, T).
  386nars_inference(_Ctx, [implication(P, M), T1], [M, T2], [P, T]):-
  387 	narz_ground(P), narz_f_abd(T1, T2, T).
  388nars_inference(_Ctx, [M, T1], [equivalence(S, M), T2], [S, T]):-
  389 	narz_ground(S), narz_f_ana(T1, T2, T).
  393nars_inference(_Ctx, [P, T1], [S, T2], [C, T]):-
  394 	C == implication(S, P), narz_f_ind(T1, T2, T).
  395nars_inference(_Ctx, [P, T1], [S, T2], [C, T]):-
  396 	C == equivalence(S, P), narz_f_com(T1, T2, T).
  397nars_inference(_Ctx, [P, T1], [S, T2], [C, T]):-
  398 	narz_reduce(conjunction([P, S]), N), N == C, narz_f_int(T1, T2, T).
  399nars_inference(_Ctx, [P, T1], [S, T2], [C, T]):-
  400 	narz_reduce(disjunction([P, S]), N), N == C, narz_f_uni(T1, T2, T).
  404nars_inference(_Ctx, [S, T1], [conjunction(L), T2], [P, T]):-
  405 	narz_ground(S), narz_ground(L), member(S, L), delete(L, S, N), narz_reduce(conjunction(N), P), narz_f_pnn(T1, T2, T).
  406nars_inference(_Ctx, [S, T1], [disjunction(L), T2], [P, T]):-
  407 	narz_ground(S), narz_ground(L), member(S, L), delete(L, S, N), narz_reduce(disjunction(N), P), narz_f_npp(T1, T2, T).
  411nars_inference(_Ctx, [implication(conjunction(L), C), T1], [M, T2], [implication(P, C), T]):-
  412 	nonvar(L), member(M, L), subtract(L, [M], A), A \= [], narz_reduce(conjunction(A), P), narz_f_ded(T1, T2, T).
  413nars_inference(_Ctx, [implication(conjunction(L), C), T1], [implication(P, C), T2], [M, T]):-
  414 	narz_ground(L), member(M, L), subtract(L, [M], A), A \= [], narz_reduce(conjunction(A), P), narz_f_abd(T1, T2, T).
  415nars_inference(_Ctx, [implication(conjunction(L), C), T1], [M, T2], [S, T]):-
  416 	S == implication(conjunction([M|L]), C), narz_f_ind(T1, T2, T).
  417
  418nars_inference(_Ctx, [implication(conjunction(Lm), C), T1], [implication(A, M), T2], [implication(P, C), T]):-
  419 	nonvar(Lm), narz_replace(Lm, M, La, A), narz_reduce(conjunction(La), P), narz_f_ded(T1, T2, T).
  420nars_inference(_Ctx, [implication(conjunction(Lm), C), T1], [implication(conjunction(La), C), T2], [implication(A, M), T]):-
  421 	nonvar(Lm), narz_replace(Lm, M, La, A), narz_f_abd(T1, T2, T).
  422nars_inference(_Ctx, [implication(conjunction(La), C), T1], [implication(A, M), T2], [implication(P, C), T]):-
  423 	nonvar(La), narz_replace(Lm, M, La, A), narz_reduce(conjunction(Lm), P), narz_f_ind(T1, T2, T).
  427nars_inference(_Ctx, [inheritance(M, P), T1], [inheritance(M, S), T2], [implication(inheritance(X, S), inheritance(X, P)), T]):-
  428 	S \= P, narz_f_ind(T1, T2, T).
  429nars_inference(_Ctx, [inheritance(P, M), T1], [inheritance(S, M), T2], [implication(inheritance(P, X), inheritance(S, X)), T]):-
  430 	S \= P, narz_f_abd(T1, T2, T).
  431nars_inference(_Ctx, [inheritance(M, P), T1], [inheritance(M, S), T2], [equivalence(inheritance(X, S), inheritance(X, P)), T]):-
  432 	S \= P, narz_f_com(T1, T2, T).
  433nars_inference(_Ctx, [inheritance(P, M), T1], [inheritance(S, M), T2], [equivalence(inheritance(P, X), inheritance(S, X)), T]):-
  434 	S \= P, narz_f_com(T1, T2, T).
  435nars_inference(_Ctx, [inheritance(M, P), T1], [inheritance(M, S), T2], [conjunction([inheritance(var(Y, []), S), inheritance(var(Y, []), P)]), T]):-
  436 	S \= P, narz_f_int(T1, T2, T).
  437nars_inference(_Ctx, [inheritance(P, M), T1], [inheritance(S, M), T2], [conjunction([inheritance(S, var(Y, [])), inheritance(P, var(Y, []))]), T]):-
  438 	S \= P, narz_f_int(T1, T2, T).
  442nars_inference(_Ctx, [implication(A, inheritance(M1, P)), T1], [inheritance(M2, S), T2], [implication(conjunction([A, inheritance(X, S)]), inheritance(X, P)), T]):-
  443 	S \= P, M1 == M2, A \= inheritance(M2, S), narz_f_ind(T1, T2, T).
  444nars_inference(_Ctx, [implication(A, inheritance(M1, P)), T1], [inheritance(M2, S), T2], [conjunction([implication(A, inheritance(var(Y, []), P)), inheritance(var(Y, []), S)]), T]):-
  445 	S \= P, M1 == M2, A \= inheritance(M2, S), narz_f_int(T1, T2, T).
  446nars_inference(_Ctx, [conjunction(L1), T1], [inheritance(M, S), T2], [implication(inheritance(Y, S), conjunction([inheritance(Y, P2)|L3])), T]):-
  447 	subtract(L1, [inheritance(M, P)], L2), L1 \= L2, S \= P, narz_dependant(P, Y, P2), narz_dependant(L2, Y, L3), narz_f_ind(T1, T2, T).
  448nars_inference(_Ctx, [conjunction(L1), T1], [inheritance(M, S), T2], [conjunction([inheritance(var(Y, []), S), inheritance(var(Y, []), P)|L2]), T]):-
  449 	subtract(L1, [inheritance(M, P)], L2), L1 \= L2, S \= P, narz_f_int(T1, T2, T).
  450
  451nars_inference(_Ctx, [implication(A, inheritance(P, M1)), T1], [inheritance(S, M2), T2], [implication(conjunction([A, inheritance(P, X)]), inheritance(S, X)), T]):-
  452 	S \= P, M1 == M2, A \= inheritance(S, M2), narz_f_abd(T1, T2, T).
  453nars_inference(_Ctx, [implication(A, inheritance(P, M1)), T1], [inheritance(S, M2), T2], [conjunction([implication(A, inheritance(P, var(Y, []))), inheritance(S, var(Y, []))]), T]):-
  454 	S \= P, M1 == M2, A \= inheritance(S, M2), narz_f_int(T1, T2, T).
  455nars_inference(_Ctx, [conjunction(L1), T1], [inheritance(S, M), T2], [implication(inheritance(S, Y), conjunction([inheritance(P2, Y)|L3])), T]):-
  456 	subtract(L1, [inheritance(P, M)], L2), L1 \= L2, S \= P, narz_dependant(P, Y, P2), narz_dependant(L2, Y, L3), narz_f_abd(T1, T2, T).
  457nars_inference(_Ctx, [conjunction(L1), T1], [inheritance(S, M), T2], [conjunction([inheritance(S, var(Y, [])), inheritance(P, var(Y, []))|L2]), T]):-
  458 	subtract(L1, [inheritance(P, M)], L2), L1 \= L2, S \= P, narz_f_int(T1, T2, T).
  462nars_inference(_Ctx, [conjunction(L1), T1], [inheritance(M, S), T2], [C, T]):-
  463 	subtract(L1, [inheritance(var(N, D), S)], L2), L1 \= L2,
  464 	replace_var(L2, var(N, D), L3, M), narz_reduce(conjunction(L3), C), narz_f_cnv(T2, T0), narz_f_ana(T1, T0, T).
  465nars_inference(_Ctx, [conjunction(L1), T1], [inheritance(S, M), T2], [C, T]):-
  466 	subtract(L1, [inheritance(S, var(N, D))], L2), L1 \= L2,
  467 	replace_var(L2, var(N, D), L3, M), narz_reduce(conjunction(L3), C), narz_f_cnv(T2, T0), narz_f_ana(T1, T0, T).
  468
  469replace_var([], _, [], _).
  470replace_var([inheritance(S1, P)|T1], S1, [inheritance(S2, P)|T2], S2):-
  471 	replace_var(T1, S1, T2, S2).
  472replace_var([inheritance(S, P1)|T1], P1, [inheritance(S, P2)|T2], P2):-
  473 	replace_var(T1, P1, T2, P2).
  474replace_all([H|T1], H1, [H|T2], H2):-
  475 	replace_var(T1, H1, T2, H2).
  476
  477
  478
  479%%% Theorems in IL:
  480
  481%NARS inheritance/2
  482inheritance(X, Y):- nars_ctx(Ctx), nars_inheritance(Ctx, X, Y).
  483
  484nars_inheritance(_Ctx, ext_intersection(Ls), P):-
  485 	narz_include([P], Ls).
  486nars_inheritance(_Ctx, S, int_intersection(Lp)):-
  487 	narz_include([S], Lp).
  488nars_inheritance(_Ctx, ext_intersection(S), ext_intersection(P)):-
  489 	narz_include(P, S), P \= [_].
  490nars_inheritance(_Ctx, int_intersection(S), int_intersection(P)):-
  491 	narz_include(S, P), S \= [_].
  492nars_inheritance(_Ctx, ext_set(S), ext_set(P)):-
  493 	narz_include(S, P).
  494nars_inheritance(_Ctx, int_set(S), int_set(P)):-
  495 	narz_include(P, S).
  496
  497nars_inheritance(_Ctx, ext_difference(S, P), S):-
  498 	narz_ground(S), narz_ground(P).
  499nars_inheritance(_Ctx, S, int_difference(S, P)):-
  500 	narz_ground(S), narz_ground(P).
  501
  502nars_inheritance(_Ctx, product(L1), R):-
  503 	narz_ground(L1), member(ext_image(R, L2), L1), narz_replace(L1, ext_image(R, L2), L2).
  504nars_inheritance(_Ctx, R, product(L1)):-
  505 	narz_ground(L1), member(int_image(R, L2), L1), narz_replace(L1, int_image(R, L2), L2).
  506
  507%NARS similarity/2
  508similarity(X, Y):- nars_ctx(Ctx), nars_similarity(Ctx, X, Y).
  509
  510nars_similarity(_Ctx, X, Y):-
  511 	narz_ground(X), narz_reduce(X, Y), X \== Y, !.
  512
  513nars_similarity(_Ctx, ext_intersection(L1), ext_intersection(L2)):-
  514 	narz_same_set(L1, L2).
  515nars_similarity(_Ctx, int_intersection(L1), int_intersection(L2)):-
  516 	narz_same_set(L1, L2).
  517nars_similarity(_Ctx, ext_set(L1), ext_set(L2)):-
  518 	narz_same_set(L1, L2).
  519nars_similarity(_Ctx, int_set(L1), int_set(L2)):-
  520 	narz_same_set(L1, L2).
  521
  522%NARS implication/2
  523implication(X, Y):- nars_ctx(Ctx), nars_implication(Ctx, X, Y).
  524
  525nars_implication(_Ctx, similarity(S, P), inheritance(S, P)).
  526nars_implication(_Ctx, equivalence(S, P), implication(S, P)).
  527
  528nars_implication(_Ctx, conjunction(L), M):-
  529 	narz_ground(L), member(M, L).
  530nars_implication(_Ctx, M, disjunction(L)):-
  531 	narz_ground(L), member(M, L).
  532
  533nars_implication(_Ctx, conjunction(L1), conjunction(L2)):-
  534 	narz_ground(L1), narz_ground(L2), subset(L2, L1).
  535nars_implication(_Ctx, disjunction(L1), disjunction(L2)):-
  536 	narz_ground(L1), narz_ground(L2), subset(L1, L2).
  537
  538nars_implication(_Ctx, inheritance(S, P), inheritance(ext_intersection(Ls), ext_intersection(Lp))):-
  539 	narz_ground(Ls), narz_ground(Lp), narz_replace(Ls, S, L, P), narz_same(L, Lp).
  540nars_implication(_Ctx, inheritance(S, P), inheritance(int_intersection(Ls), int_intersection(Lp))):-
  541 	narz_ground(Ls), narz_ground(Lp), narz_replace(Ls, S, L, P), narz_same(L, Lp).
  542nars_implication(_Ctx, similarity(S, P), similarity(ext_intersection(Ls), ext_intersection(Lp))):-
  543 	narz_ground(Ls), narz_ground(Lp), narz_replace(Ls, S, L, P), narz_same(L, Lp).
  544nars_implication(_Ctx, similarity(S, P), similarity(int_intersection(Ls), int_intersection(Lp))):-
  545 	narz_ground(Ls), narz_ground(Lp), narz_replace(Ls, S, L, P), narz_same(L, Lp).
  546
  547nars_implication(_Ctx, inheritance(S, P), inheritance(ext_difference(S, M), ext_difference(P, M))):-
  548 	narz_ground(M).
  549nars_implication(_Ctx, inheritance(S, P), inheritance(int_difference(S, M), int_difference(P, M))):-
  550 	narz_ground(M).
  551nars_implication(_Ctx, similarity(S, P), similarity(ext_difference(S, M), ext_difference(P, M))):-
  552 	narz_ground(M).
  553nars_implication(_Ctx, similarity(S, P), similarity(int_difference(S, M), int_difference(P, M))):-
  554 	narz_ground(M).
  555nars_implication(_Ctx, inheritance(S, P), inheritance(ext_difference(M, P), ext_difference(M, S))):-
  556 	narz_ground(M).
  557nars_implication(_Ctx, inheritance(S, P), inheritance(int_difference(M, P), int_difference(M, S))):-
  558 	narz_ground(M).
  559nars_implication(_Ctx, similarity(S, P), similarity(ext_difference(M, P), ext_difference(M, S))):-
  560 	narz_ground(M).
  561nars_implication(_Ctx, similarity(S, P), similarity(int_difference(M, P), int_difference(M, S))):-
  562 	narz_ground(M).
  563
  564nars_implication(_Ctx, inheritance(S, P), negation(inheritance(S, ext_difference(M, P)))):-
  565 	narz_ground(M).
  566nars_implication(_Ctx, inheritance(S, ext_difference(M, P)), negation(inheritance(S, P))):-
  567 	narz_ground(M).
  568nars_implication(_Ctx, inheritance(S, P), negation(inheritance(int_difference(M, S), P))):-
  569 	narz_ground(M).
  570nars_implication(_Ctx, inheritance(int_difference(M, S), P), negation(inheritance(S, P))):-
  571 	narz_ground(M).
  572
  573nars_implication(_Ctx, inheritance(S, P), inheritance(ext_image(S, M), ext_image(P, M))):-
  574 	narz_ground(M).
  575nars_implication(_Ctx, inheritance(S, P), inheritance(int_image(S, M), int_image(P, M))):-
  576 	narz_ground(M).
  577nars_implication(_Ctx, inheritance(S, P), inheritance(ext_image(M, Lp), ext_image(M, Ls))):-
  578 	narz_ground(Ls), narz_ground(Lp), append(L1, [S|L2], Ls), append(L1, [P|L2], Lp).
  579nars_implication(_Ctx, inheritance(S, P), inheritance(int_image(M, Lp), int_image(M, Ls))):-
  580 	narz_ground(Ls), narz_ground(Lp), append(L1, [S|L2], Ls), append(L1, [P|L2], Lp).
  581
  582nars_implication(_Ctx, negation(M), negation(conjunction(L))):-
  583 	narz_include([M], L).
  584nars_implication(_Ctx, negation(disjunction(L)), negation(M)):-
  585 	narz_include([M], L).
  586
  587nars_implication(_Ctx, implication(S, P), implication(conjunction(Ls), conjunction(Lp))):-
  588 	narz_ground(Ls), narz_ground(Lp), narz_replace(Ls, S, L, P), narz_same(L, Lp).
  589nars_implication(_Ctx, implication(S, P), implication(disjunction(Ls), disjunction(Lp))):-
  590 	narz_ground(Ls), narz_ground(Lp), narz_replace(Ls, S, L, P), narz_same(L, Lp).
  591nars_implication(_Ctx, equivalence(S, P), equivalence(conjunction(Ls), conjunction(Lp))):-
  592 	narz_ground(Ls), narz_ground(Lp), narz_replace(Ls, S, L, P), narz_same(L, Lp).
  593nars_implication(_Ctx, equivalence(S, P), equivalence(disjunction(Ls), disjunction(Lp))):-
  594 	narz_ground(Ls), narz_ground(Lp), narz_replace(Ls, S, L, P), narz_same(L, Lp).
  595
  596
  597%NARS equivalence/2
  598equivalence(X, Y):- nars_ctx(Ctx), nars_equivalence(Ctx, X, Y).
  599
  600nars_equivalence(_Ctx, X, Y):-
  601 	narz_ground(X), narz_reduce(X, Y), X \== Y, !.
  602
  603nars_equivalence(_Ctx, similarity(S, P), similarity(P, S)).
  604
  605nars_equivalence(_Ctx, inheritance(S, ext_set([P])), similarity(S, ext_set([P]))).
  606nars_equivalence(_Ctx, inheritance(int_set([S]), P), similarity(int_set([S]), P)).
  607
  608nars_equivalence(Ctx, inheritance(S, ext_intersection(Lp)), conjunction(L)):-
  609 	findall(nars_inheritance(Ctx, S, P), member(P, Lp), L).
  610nars_equivalence(Ctx, inheritance(int_intersection(Ls), P), conjunction(L)):-
  611 	findall(nars_inheritance(Ctx, S, P), member(S, Ls), L).
  612
  613nars_equivalence(_Ctx, inheritance(S, ext_difference(P1, P2)),
  614 	    conjunction([inheritance(S, P1), negation(inheritance(S, P2))])).
  615nars_equivalence(_Ctx, inheritance(int_difference(S1, S2), P),
  616 	    conjunction([inheritance(S1, P), negation(inheritance(S2, P))])).
  617
  618nars_equivalence(_Ctx, inheritance(product(Ls), product(Lp)), conjunction(L)):-
  619 	equ_product(Ls, Lp, L).
  620
  621nars_equivalence(_Ctx, inheritance(product([S|L]), product([P|L])), inheritance(S, P)):-
  622 	narz_ground(L).
  623nars_equivalence(Ctx, inheritance(S, P), inheritance(product([H|Ls]), product([H|Lp]))):-
  624 	narz_ground(H), nars_equivalence(Ctx, inheritance(product(Ls), product(Lp)), inheritance(S, P)).
  625
  626nars_equivalence(_Ctx, inheritance(product(L), R), inheritance(T, ext_image(R, L1))):-
  627 	narz_replace(L, T, L1).
  628nars_equivalence(_Ctx, inheritance(R, product(L)), inheritance(int_image(R, L1), T)):-
  629 	narz_replace(L, T, L1).
  630
  631nars_equivalence(_Ctx, equivalence(S, P), equivalence(P, S)).
  632
  633nars_equivalence(_Ctx, equivalence(negation(S), P), equivalence(negation(P), S)).
  634
  635nars_equivalence(_Ctx, conjunction(L1), conjunction(L2)):-
  636 	narz_same_set(L1, L2).
  637nars_equivalence(_Ctx, disjunction(L1), disjunction(L2)):-
  638 	narz_same_set(L1, L2).
  639
  640nars_equivalence(Ctx, implication(S, conjunction(Lp)), conjunction(L)):-
  641 	findall(nars_implication(Ctx, S, P), member(P, Lp), L).
  642nars_equivalence(Ctx, implication(disjunction(Ls), P), conjunction(L)):-
  643 	findall(nars_implication(Ctx, S, P), member(S, Ls), L).
  644
  645nars_equivalence(Ctx, T1, T2):-
  646 	not(atom(T1)), not(atom(T2)), narz_ground(T1), narz_ground(T2),
  647 	T1 =.. L1, T2 =.. L2, nars_equivalence_list(Ctx, L1, L2).
  648
  649nars_equivalence_list(_Ctx, L, L).
  650nars_equivalence_list(Ctx, [H|L1], [H|L2]):-
  651 	nars_equivalence_list(Ctx, L1, L2).
  652nars_equivalence_list(Ctx, [H1|L1], [H2|L2]):-
  653 	nars_similarity(Ctx, H1, H2), nars_equivalence_list(Ctx, L1, L2).
  654nars_equivalence_list(Ctx, [H1|L1], [H2|L2]):-
  655 	nars_equivalence(Ctx, H1, H2), nars_equivalence_list(Ctx, L1, L2).
  656
  657% compound termnars_structurereduction
  658
  659narz_reduce(similarity(ext_set([S]), ext_set([P])), similarity(S, P)):-
  660 	!.
  661narz_reduce(similarity(int_set([S]), int_set([P])), similarity(S, P)):-
  662 	!.
  663
  664narz_reduce(instance(S, P), inheritance(ext_set([S]), P)):-
  665 	!.
  666narz_reduce(property(S, P), inheritance(S, int_set([P]))):-
  667 	!.
  668narz_reduce(inst_prop(S, P), inheritance(ext_set([S]), int_set([P]))):-
  669 	!.
  670
  671narz_reduce(ext_intersection([T]), T):-
  672 	!.
  673narz_reduce(int_intersection([T]), T):-
  674 	!.
  675
  676narz_reduce(ext_intersection([ext_intersection(L1), ext_intersection(L2)]), ext_intersection(L)):-
  677 	union(L1, L2, L), !.
  678narz_reduce(ext_intersection([ext_intersection(L1), L2]), ext_intersection(L)):-
  679 	union(L1, [L2], L), !.
  680narz_reduce(ext_intersection([L1, ext_intersection(L2)]), ext_intersection(L)):-
  681 	union([L1], L2, L), !.
  682narz_reduce(ext_intersection([ext_set(L1), ext_set(L2)]), ext_set(L)):-
  683 	intersection(L1, L2, L), !.
  684narz_reduce(ext_intersection([int_set(L1), int_set(L2)]), int_set(L)):-
  685 	union(L1, L2, L), !.
  686
  687narz_reduce(int_intersection([int_intersection(L1), int_intersection(L2)]), int_intersection(L)):-
  688 	union(L1, L2, L), !.
  689narz_reduce(int_intersection([int_intersection(L1), L2]), int_intersection(L)):-
  690 	union(L1, [L2], L), !.
  691narz_reduce(int_intersection([L1, int_intersection(L2)]), int_intersection(L)):-
  692 	union([L1], L2, L), !.
  693narz_reduce(int_intersection([int_set(L1), int_set(L2)]), int_set(L)):-
  694 	intersection(L1, L2, L), !.
  695narz_reduce(int_intersection([ext_set(L1), ext_set(L2)]), ext_set(L)):-
  696 	union(L1, L2, L), !.
  697
  698narz_reduce(ext_difference(ext_set(L1), ext_set(L2)), ext_set(L)):-
  699 	subtract(L1, L2, L), !.
  700narz_reduce(int_difference(int_set(L1), int_set(L2)), int_set(L)):-
  701 	subtract(L1, L2, L), !.
  702
  703narz_reduce(product(product(L), T), product(L1)):-
  704 	append(L, [T], L1), !.
  705
  706narz_reduce(ext_image(product(L1), L2), T1):-
  707 	member(T1, L1), narz_replace(L1, T1, L2), !.
  708narz_reduce(int_image(product(L1), L2), T1):-
  709 	member(T1, L1), narz_replace(L1, T1, L2), !.
  710
  711narz_reduce(negation(negation(S)), S):-
  712 	!.
  713
  714narz_reduce(conjunction([T]), T):-
  715 	!.
  716narz_reduce(disjunction([T]), T):-
  717 	!.
  718
  719narz_reduce(conjunction([conjunction(L1), conjunction(L2)]), conjunction(L)):-
  720 	union(L1, L2, L), !.
  721narz_reduce(conjunction([conjunction(L1), L2]), conjunction(L)):-
  722 	union(L1, [L2], L), !.
  723narz_reduce(conjunction([L1, conjunction(L2)]), conjunction(L)):-
  724 	union([L1], L2, L), !.
  725
  726narz_reduce(disjunction(disjunction(L1), disjunction(L2)), disjunction(L)):-
  727 	union(L1, L2, L), !.
  728narz_reduce(disjunction(disjunction(L1), L2), disjunction(L)):-
  729 	union(L1, [L2], L), !.
  730narz_reduce(disjunction(L1, disjunction(L2)), disjunction(L)):-
  731 	union([L1], L2, L), !.
  732
  733narz_reduce(X, X).
  734
  735
  736%%% Argument processing
  737
  738equ_product([], [], []).
  739equ_product([T|Ls], [T|Lp], L):-
  740 	equ_product(Ls, Lp, L), !.
  741equ_product([S|Ls], [P|Lp], [inheritance(S, P)|L]):-
  742 	equ_product(Ls, Lp, L).
  743
  744narz_same_set(L1, L2):-
  745 	L1 \== [], L1 \== [_], narz_same(L1, L2), L1 \== L2.
  746
  747narz_same([], []).
  748narz_same(L, [H|T]):-
  749 	member(H, L), subtract(L, [H], L1), narz_same(L1, T).
  750
  751narz_include(L1, L2):-
  752 	narz_ground(L2), include1(L1, L2), L1 \== [], L1 \== L2.
  753
  754 include1([], _).
  755 include1([H|T1], [H|T2]):-
  756 	include1(T1, T2).
  757 include1([H1|T1], [H2|T2]):-
  758 	H2 \== H1, include1([H1|T1], T2).
  759
  760narz_not_member(_, []).
  761narz_not_member(C, [C|_]):-  !, fail.
  762narz_not_member([S, T], [[S1, T]|_]):- nars_equivalence(_Ctx, S, S1), !, fail.
  763narz_not_member(C, [_|L]):- narz_not_member(C, L).
  764
  765narz_replace([T|L], T, [nil|L]).
  766narz_replace([H|L], T, [H|L1]):-
  767 	narz_replace(L, T, L1).
  768
  769narz_replace([H1|T], H1, [H2|T], H2).
  770narz_replace([H|T1], H1, [H|T2], H2):-
  771 	narz_replace(T1, H1, T2, H2).
  772
  773narz_dependant(var(V, L), Y, var(V, [Y|L])):-
  774 	!.
  775narz_dependant([H|T], Y, [H1|T1]):-
  776 	narz_dependant(H, Y, H1), narz_dependant(T, Y, T1), !.
  777narz_dependant(inheritance(S, P), Y, inheritance(S1, P1)):-
  778 	narz_dependant(S, Y, S1), narz_dependant(P, Y, P1), !.
  779narz_dependant(ext_image(R, A), Y, ext_image(R, A1)):-
  780 	narz_dependant(A, Y, A1), !.
  781narz_dependant(int_image(R, A), Y, int_image(R, A1)):-
  782 	narz_dependant(A, Y, A1), !.
  783narz_dependant(X, _, X).
  784
  785
  786%%% Truth-value functions
  787
  788narz_f_rev([F1, C1], [F2, C2], [F, C]):-
  789      C1 < 1,
  790      C2 < 1,
  791 	M1 is C1 / (1 - C1),
  792 	M2 is C2 / (1 - C2),
  793 	F is (M1 * F1 + M2 * F2) / (M1 + M2),
  794 	C is (M1 + M2) / (M1 + M2 + 1).
  795
  796narz_f_exp([F, C], E):-
  797 	E is C * (F - 0.5) + 0.5.
  798
  799narz_f_neg([F1, C1], [F, C1]):-
  800 	u_not(F1, F).
  801
  802narz_f_cnv([F1, C1], [1, C]):-
  803     u_and([F1, C1], W),
  804 	u_w2c(W, C).
  805
  806narz_f_cnt([F1, C1], [0, C]):-
  807 	u_not(F1, F0),
  808     u_and([F0, C1], W),
  809 	u_w2c(W, C).
  810
  811narz_f_ded([F1, C1], [F2, C2], [F, C]):-
  812 	u_and([F1, F2], F),
  813 	u_and([C1, C2, F], C).
  814
  815narz_f_ana([F1, C1], [F2, C2], [F, C]):-
  816 	u_and([F1, F2], F),
  817 	u_and([C1, C2, F2], C).
  818
  819narz_f_res([F1, C1], [F2, C2], [F, C]):-
  820 	u_and([F1, F2], F),
  821 	u_or([F1, F2], F0),
  822 	u_and([C1, C2, F0], C).
  823
  824narz_f_abd([F1, C1], [F2, C2], [F2, C]):-
  825 	u_and([F1, C1, C2], W),
  826 	u_w2c(W, C).
  827
  828narz_f_ind(T1, T2, T):-
  829 	narz_f_abd(T2, T1, T).
  830
  831narz_f_exe([F1, C1], [F2, C2], [1, C]):-
  832 	u_and([F1, C1, F2, C2], W),
  833 	u_w2c(W, C).
  834
  835narz_f_com([0, _C1], [0, _C2], [0, 0]).
  836narz_f_com([F1, C1], [F2, C2], [F, C]):-
  837 	u_or([F1, F2], F0),
  838 	F0 > 0,
  839 	F is F1 * F2 / F0,
  840 	u_and([F0, C1, C2], W),
  841 	u_w2c(W, C).
  842
  843narz_f_int([F1, C1], [F2, C2], [F, C]):-
  844 	u_and([F1, F2], F),
  845 	u_and([C1, C2], C).
  846
  847narz_f_uni([F1, C1], [F2, C2], [F, C]):-
  848 	u_or([F1, F2], F),
  849 	u_and([C1, C2], C).
  850
  851narz_f_dif([F1, C1], [F2, C2], [F, C]):-
  852 	u_not(F2, F0),
  853 	u_and([F1, F0], F),
  854 	u_and([C1, C2], C).
  855
  856narz_f_pnn([F1, C1], [F2, C2], [F, C]):-
  857 	u_not(F2, F2n),
  858 	u_and([F1, F2n], Fn),
  859 	u_not(Fn, F),
  860 	u_and([Fn, C1, C2], C).
  861
  862narz_f_npp([F1, C1], [F2, C2], [F, C]):-
  863 	u_not(F1, F1n),
  864 	u_and([F1n, F2], F),
  865 	u_and([F, C1, C2], C).
  866
  867narz_f_pnp([F1, C1], [F2, C2], [F, C]):-
  868 	u_not(F2, F2n),
  869 	u_and([F1, F2n], F),
  870 	u_and([F, C1, C2], C).
  871
  872narz_f_nnn([F1, C1], [F2, C2], [F, C]):-
  873 	u_not(F1, F1n),
  874 	u_not(F2, F2n),
  875 	u_and([F1n, F2n], Fn),
  876 	u_not(Fn, F),
  877 	u_and([Fn, C1, C2], C).
  878
  879% Utility functions
  880
  881u_not(N0, N):-
  882 	N is (1 - N0), !.
  883
  884u_and([N], N).
  885u_and([N0 | Nt], N):-
  886 	u_and(Nt, N1), N is N0 * N1, !.
  887
  888u_or([N], N).
  889u_or([N0 | Nt], N):-
  890 	u_or(Nt, N1), N is (N0 + N1 - N0 * N1), !.
  891
  892u_w2c(W, C):-
  893 	K = 1, C is (W / (W + K)), !.
  894
  895
  896%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  897%memory.pl
  898
  899%11.1.2 State accumulation using engines - https://www.swi-prolog.org/pldoc/man?section=engine-state
  900:- use_module(library(heaps)).  901
  902create_heap(E) :- empty_heap(H), engine_create(_, update_heap(H), E).
  903update_heap(H) :- engine_fetch(Command), ( update_heap(Command, Reply, H, H1) ->  true; H1 = H, Reply = false ), engine_yield(Reply), update_heap(H1).
  904
  905update_heap(add(Priority, Key), true, H0, H) :- add_to_heap(H0, Priority, Key, H).
  906update_heap(get(Priority, Key), Priority-Key, H0, H) :- get_from_heap(H0, Priority, Key, H).
  907
  908heap_add(Priority, Key, E) :- engine_post(E, add(Priority, Key), true).
  909
  910heap_get(Priority, Key, E) :- engine_post(E, get(Priority, Key), Priority-Key).
  911
  912%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  913%control.pl
  914
  915priority([_, [F,C]], P) :- narz_f_exp([F, C], E), P is E.
  916
  917input_event(Event) :- heap_add(1.0, Event, belief_events_queue).
  918
  919derive_event(Event) :- priority(Event, P), heap_add(P, Event, belief_events_queue).
  920
  921inference_step(_) :- (heap_get(_Priority, Event, belief_events_queue),
  922                      heap_get(Priority2, Event2, belief_events_queue),
  923                      heap_add(Priority2, Event2, belief_events_queue), %undo removal of the second premise (TODO)
  924                      inference(Event,Event2,Conclusion), 
  925                      derive_event(Conclusion),
  926                      write(Conclusion), nl
  927                     ; true ).
  928
  929nars_main :- create_heap(belief_events_queue), nars_main(1).
  930nars_main(T) :- read_nal(X),
  931     (X = 1, write("performing 1 inference steps:"), nl, 
  932     inference_step(T), write("done with 1 additional inference steps."), nl,  
  933       nars_main(T+1) ; 
  934       X \= 1, write("Input: "), write(X), nl, input_event(X), nars_main(T+1)).
  935
  936% read_nal(X):- read(X).
  937read_nal(X):- nal_read_clause(current_input, X).
  938
  939%test:
  940%nars_main.
  941%[inheritance(cat,animal), [1.0, 0.9]].
  942%[inheritance(animal,being), [1.0, 0.9]].
  943%1.
  944%output:
  945%performing 1 inference steps:
  946%[inheritance(cat,being),[1.0,0.81]]
  947%done with 1 additional inference steps.
  948
  949
  950:-  fixup_exports.