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
   20%:- set_fileAssertMt(baseKB).
   21
   22:- asserta_new(user:file_search_path(pldata,'/opt/cyc/')).   23:- asserta_new(user:file_search_path(pldata,library(pldata))).   24:- asserta_new(user:file_search_path(logicmoo,library('.'))).   25
   26:- absolute_file_name(library('../ext/pldata/'),Dir,[file_type(directory)]),
   27   asserta_new(user:file_search_path(pldata,Dir)).   28
   29:- absolute_file_name(library('../ext/'),Dir,[file_type(directory)]),
   30   asserta_new(user:file_search_path(logicmoo,Dir)).   31
   32:- gripe_time(60,baseKB:ensure_loaded(library('logicmoo/plarkc/logicmoo_i_cyc_rewriting'))).   33:- gripe_time(60,baseKB:ensure_loaded(library('logicmoo/plarkc/logicmoo_u_cyc_kb_tinykb'))).   34:- gripe_time(60,baseKB:ensure_loaded(library('logicmoo/plarkc/logicmoo_i_cyc_kb'))).   35% :- add_library_search_path('./logicmoo/plarkc/',[ 'logicmoo_i_*.pl']).
   36
   37/*
   38Before I continue I rather ensure I am using the same terminolgy as the rest
   39First I need to understand what you see as the difference between FOL and 2-Sorted FOL
   40Are both Henkin?
   41Also is FOL,  1-Sorted FOL or non-Sorted FOL?
   42Between 2-Sorted FOL and a 1-Sorted FOL
   43Between 3-Sorted FOL and a 2-Sorted FOL
   44well what i meant is that Full SOL *should* be more expressive than basic FOL 
   45in fact i have no doubts SOL *is* more expressive if it is extending basic FOL  
   46but make basic FOL extremely expressive by allowing to exist a: 2-Sorted FOL 
   47I 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 
   48
   49I refer the "expressivness", I mean the ablity thru syntactical expression to:
   501) say anything desired and predict exactly how a reasoner will understand the new expression
   512) the ability to change the default supertype ("Class") that unqualified foralls assume to be selecting from
   523) say things the reasoner will be able to interpret subsumption to apply this new expression to other expressions: refered to as "Class"
   534) Extend [dis]equality
   545) quantify over bags of axioms and other exisiting content: John McCarthy 1982(?) named "Microtheory"s
   55
   56Next Inside each "Microtheory"
   57
   586) Visiblity between Microtheories
   596a) When visibility may happen at all..  
   606b) How the Classes may change when one Microtheory sees into another
   617) create and destroy hypothetical Microtheoies per single logical expression
   628) Ability to manipulate each proof by treating it as we do our "bag of assertions/axioms"
   639) Do 2-5 locally to each MT
   64   
   65   
   66
   67MLTT = is an extension to control the u ability to
   68
   69*/
   70
   71:- dynamic(baseKB:tinyKB/3).   72:- multifile(baseKB:tinyKB/3).   73:- system:import(baseKB:tinyKB/3).   74
   75%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   76% SETUP CYC KB EXTENSIONS
   77%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   78
   79loadNewTiny:-  \+ exists_file(tiny_kb_cache),
   80  tell(tiny_kb_cache),
   81  format('~q.~n',[:- set_how_virtualize_file(false)]),
   82  format('~q.~n',[:- multifile(tiny_kb/3)]),
   83  format('~q.~n',[:-   dynamic(tiny_kb/3)]),
   84  format('~q.~n',[:- style_check(-singleton)]),
   85  forall(call(call,tinyKB,C,MT,STR),
   86        must(( (tinykb_assertion_recipe_w(C,CycLOut),
   87         format('~q.~n',[tiny_kb(CycLOut,MT,STR)]),
   88         ignore((C\=@=CycLOut,dmsg(tiny_kb(CycLOut,MT,STR)))))))),
   89  told,
   90  consult(tiny_kb_cache).
   91
   92loadNewTiny:- consult(tiny_kb_cache).
   93
   94%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   95% SAVE CYC KB EXTENSIONS
   96%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   97%:- after_init(loadNewTiny).
   98
   99%:- after_init(baseKB:qsave_lm(lm_repl3)).
  100
  101
  102
  103:- if(false).  104:- user:use_module(library('file_scope')).  105:- baseKB:disable_mpred_expansion.  106 % :- set_prolog_flag(subclause_expansion,false).
  107:- if(exists_source(pldata('kb_7166.qlf'))).  108:- wdmsg("loading kb_7166").  109:- set_prolog_flag_until_eof(do_renames,term_expansion).  110:- ensure_loaded(pldata('kb_7166.qlf')).  111:- else.  112:- wdmsg("qcompile kb_7166").  113%:- set_prolog_flag_until_eof(do_renames,term_expansion).
  114:- load_files(pldata(kb_7166),[if(not_loaded),qcompile(auto)]).  115:- endif.  116:- wdmsg("done loading kb_7166").  117:- set_module(kb_7166:class(library)).  118:- set_module(class(library)).  119:- enable_mpred_expansion.  120 % :- set_prolog_flag(subclause_expansion,true).
  121:- endif.