1/* <module> logicmoo_plarkc - special module hooks into the logicmoo engine allow
    2%   clif syntax to be recocogized via our CycL/KIF handlers 
    3% 
    4% Logicmoo Project: A LarKC Server written in Prolog
    5% Maintainer: Douglas Miles
    6% Dec 13, 2035
    7%
    8*/
    9:- module(logicmoo_plarkc,[]).   10
   11:- ensure_loaded(library(logicmoo_lib)).   12
   13:- multifile(baseKB:cycBetween/3).   14:- dynamic(baseKB:cycBetween/3).   15:- baseKB:export(baseKB:cycBetween/3).   16:- system:import(baseKB:cycBetween/3).   17
   18:- system:reexport(library(logicmoo_clif)).   19:- set_fileAssertMt(baseKB).   20
   21:- asserta_new(user:file_search_path(pldata,'/opt/cyc/')).   22:- asserta_new(user:file_search_path(pldata,library(pldata))).   23:- asserta_new(user:file_search_path(logicmoo,library('.'))).   24:- gripe_time(60,baseKB:ensure_loaded(library('logicmoo/plarkc/logicmoo_i_cyc_rewriting'))).   25:- gripe_time(60,baseKB:ensure_loaded(library('logicmoo/plarkc/logicmoo_u_cyc_kb_tinykb'))).   26:- gripe_time(60,baseKB:ensure_loaded(library('logicmoo/plarkc/logicmoo_i_cyc_kb'))).   27% :- add_library_search_path('./logicmoo/plarkc/',[ 'logicmoo_i_*.pl']).
   28
   29/*
   30Before I continue I rather ensure I am using the same terminolgy as the rest
   31First I need to understand what you see as the difference between FOL and 2-Sorted FOL
   32Are both Henkin?
   33Also is FOL,  1-Sorted FOL or non-Sorted FOL?
   34Between 2-Sorted FOL and a 1-Sorted FOL
   35Between 3-Sorted FOL and a 2-Sorted FOL
   36well what i meant is that Full SOL *should* be more expressive than basic FOL 
   37in fact i have no doubts SOL *is* more expressive if it is extending basic FOL  
   38but make basic FOL extremely expressive by allowing to exist a: 2-Sorted FOL 
   39I would like to belive there could be a possiblity of add SOL to 2-Sorted FOL  the same way as SOL can be added to non sorted-FOL 
   40
   41I refer the "expressivness", I mean the ablity thru syntactical expression to:
   421) say anything desired and predict exactly how a reasoner will understand the new expression
   432) the ability to change the default supertype ("Class") that unqualified foralls assume to be selecting from
   443) say things the reasoner will be able to interpret subsumption to apply this new expression to other expressions: refered to as "Class"
   454) Extend [dis]equality
   465) quantify over bags of axioms and other exisiting content: John McCarthy 1982(?) named "Microtheory"s
   47
   48Next Inside each "Microtheory"
   49
   506) Visiblity between Microtheories
   516a) When visibility may happen at all..  
   526b) How the Classes may change when one Microtheory sees into another
   537) create and destroy hypothetical Microtheoies per single logical expression
   548) Ability to manipulate each proof by treating it as we do our "bag of assertions/axioms"
   559) Do 2-5 locally to each MT
   56   
   57   
   58
   59MLTT = is an extension to control the u ability to
   60
   61*/
   62
   63%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   64% SETUP CYC KB EXTENSIONS
   65%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   66
   67loadNewTiny:-  \+ exists_file(tiny_kb_cache),
   68  tell(tiny_kb_cache),
   69  format('~q.~n',[:- asserta(baseKB:ignore_file_mpreds(tiny_kb_cache))]),
   70  format('~q.~n',[:- multifile(tiny_kb/3)]),
   71  format('~q.~n',[:-   dynamic(tiny_kb/3)]),
   72  format('~q.~n',[:- style_check(-singleton)]),
   73  forall(tinyKB(C,MT,STR),
   74        must(( (tinykb_assertion_recipe_w(C,CycLOut),
   75         format('~q.~n',[tiny_kb(CycLOut,MT,STR)]),
   76         ignore((C\=@=CycLOut,dmsg(tiny_kb(CycLOut,MT,STR)))))))),
   77  told,
   78  consult(tiny_kb_cache).
   79loadNewTiny:- consult(tiny_kb_cache).
   80
   81%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   82% SAVE CYC KB EXTENSIONS
   83%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   84:- after_boot(loadNewTiny).   85
   86:- after_boot(baseKB:qsave_lm(lm_repl3)).   87
   88
   89
   90:- if(false).   91:- user:use_module(library('file_scope')).   92:- baseKB:disable_mpred_expansion.   93 % :- set_prolog_flag(subclause_expansion,false).
   94:- if(exists_source(pldata('kb_7166.qlf'))).   95:- wdmsg("loading kb_7166").   96:- set_prolog_flag_until_eof(do_renames,term_expansion).   97:- ensure_loaded(pldata('kb_7166.qlf')).   98:- else.   99:- wdmsg("qcompile kb_7166").  100%:- set_prolog_flag_until_eof(do_renames,term_expansion).
  101:- load_files(pldata(kb_7166),[if(not_loaded),qcompile(auto)]).  102:- endif.  103:- wdmsg("done loading kb_7166").  104:- set_module(kb_7166:class(library)).  105:- set_module(class(library)).  106:- enable_mpred_expansion.  107 % :- set_prolog_flag(subclause_expansion,true).
  108:- endif.