API tools faq
paste
Advertisement
logicmoo

CALC

logicmoo
Aug 16th, 2017
306
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Prolog 7.29 KB | None | 0 0
raw download clone embed print report
  1. /*
  2.  
  3.  CALCULATOR WORLD
  4.  
  5. [13:28] * dmiles attempts to write a program in FOL today! just a simple 14 key caclulator
  6. [13:29] <dmiles> just to discover the hellishness
  7. [13:29] <anniepoo_> the calculator believes that X is 7?
  8. [13:31] <dmiles> yes
  9. [13:31] <dmiles> well the other parts is believing the key buffer represents cerain values and so forth
  10. [13:32] <dmiles> and even believing there are keys to be pressed
  11.  
  12.   part of why i doing the calculator (outside of a test case for logicmoo/prologmud).. is it has been belived that programs might be hard to express physically
  13.  
  14. */
  15.  
  16. :_ include(test_header).
  17.  
  18. % =================================================================================
  19. % Set our engine up
  20. % =================================================================================
  21.  
  22. :_ set_lang(clif).
  23. :_ begin_pfc.
  24.  
  25. % deduce instances from usages in args having the effect of deducing human,dwelling,beverage_class are classes
  26. ==> feature_setting(make_wff,true).
  27. ==> feature_setting(add_admitted_arguments,true).
  28. % set truth maintainance system to remove previous assertions that new assertions disagree with
  29. ==> feature_setting(tms_mode,remove_conflicting).
  30. % i been resisting the urge to expand the 'dictoo' language (of one of my packs) into a scripting language for prolog.
  31.  
  32. :_ set_prolog_flag(runtime_debug,3). % mention it when we remove previous assertions
  33.  
  34. :_ set_prolog_flag_until_eof(do_renames,mpred_expansion).
  35.  
  36. :_ kif_compile.
  37.  
  38.  
  39. % =================================================================================
  40. % Begin program
  41. % =================================================================================
  42.  
  43. % Create out 14 keys
  44. exists(Key,labeled(Key,"1")). exists(Key,labeled(Key,"2")).
  45. exists(Key,labeled(Key,"3")). exists(Key,labeled(Key,"4")).
  46. exists(Key,labeled(Key,"5")). exists(Key,labeled(Key,"6")).
  47. exists(Key,labeled(Key,"7")). exists(Key,labeled(Key,"8")).
  48. exists(Key,labeled(Key,"9")). exists(Key,labeled(Key,"0")).
  49. exists(Key,labeled(Key,"+")). exists(Key,labeled(Key,"_")).
  50. exists(Key,labeled(Key,"=")). exists(Key,labeled(Key,"CLR")).
  51.  
  52. % Make each key unique depending on its label
  53. forall([Key1,Key2,Label1,Label2],
  54.   labeled(Key1,Label1) & labeled(Key2,Label2) & different(Label1,Label2) => different(Key1,Key2)).
  55.  
  56. % Let same/2 be our unification identify
  57. forall(X,same(X,X)).    
  58.  
  59. % same/2 implies not differnt
  60. forall([X,Y], same(X,Y) => ~ different(X,Y)).
  61.  
  62. % Note all unquantified vars will be universal from here on out
  63. subclass(S,C) & isa(I,S) => isa(I,C).
  64.  
  65. % an accumulator is a numeric buffer
  66. subclass(accumulator,numbuffer).
  67.  
  68. % a display is a numeric buffer
  69. subclass(display,numbuffer).
  70.  
  71. % numeric buffer and operation buffer are buffers
  72. subclass(numbuffer,buffer). subclass(opbuffer,buffer).
  73.  
  74. % Create some buffers
  75. exists(X,isa(X,accumulator)).
  76. exists(X,isa(X,display)).
  77. exists(X,isa(X,opbuffer)).
  78.  
  79. /*
  80. Extra TODO ?
  81.  
  82. define how a buffer is shown in screen locations
  83. exactly(10,X, isa(X,screenLocation)).
  84.  
  85. */
  86.  
  87. % All number buffers have a, inital value of 0
  88. forall(X,isa(X,numbuffer) => initalValue(X,0)).
  89.  
  90. % exists an initial world
  91. exists(C,initialWorld(C)).
  92.  
  93. % initial world is populated by inital values
  94. initalValue(N,V) & initialWorld(W) =>  currentValue(W,N,V).
  95.  
  96. % All numeric buffers have a value
  97. forall(W,forall(N,exists(V,isa(N,numbuffer) & world(W) => currentValue(W,N,V))).
  98.  
  99. % Op buffer is intialized to null
  100. forall(X,isa(X,opbuffer) => initalValue(X,null)).
  101.  
  102. % exists a current world (Fluent 1)
  103. exists(C,currentWorld(C)).
  104.  
  105.  
  106. nextWorld(C,N)=> isa(C,world) & isa(C,world).
  107.   => currentValue
  108.  
  109.  
  110. % CTL or LTL version of automation?
  111.  
  112. currentWorld(C) & onEvent(Evt,Props) =>
  113.    exists(W,
  114.       isa(W,world)
  115.     & nextWorld(C,W)) ....
  116.    
  117.  
  118.  
  119. % after "CLR" is pressed re_init the buffers
  120. onEvent(pressed("CLR"), forall([N,V], initalValue(N,V) => currentValue(N,V))).
  121.  
  122. % after "=" is pressed the "accumulator" buffer is shown.
  123.  
  124. % after "+" or "_" is pressed the  
  125.  
  126.  
  127.  
  128.  
  129.  
  130.  
  131.  
  132.  
  133.  
  134. my_minus_one(N,M) <=>  (N > 1)  &  (M = N-1).
  135.  
  136. % Lits in KBs are considered true
  137. consistent(W) <=> min_lits(1, W) .
  138.  
  139. exactly_N_lits(1,W) <=>
  140.  exists([W,Prop],  
  141.     (   true_in_world(Prop,W)
  142.       & ~exists(Other_Prop,
  143.            (  true_in_world(Other_Prop,W)
  144.              & ~equiv(W,Other_Prop,Prop))))) .
  145.  
  146. exactly_N_lits(2,W) <=>
  147.  exists([W,Prop1,Prop2],  
  148.   (  true_in_world(Prop1,W)
  149.    & true_in_world(Prop2,W)
  150.    & ~equiv(W,Prop1,Prop2)  
  151.    & ~ exists(Other_Prop,
  152.          (  true_in_world(Other_Prop,W)
  153.           & ~equiv(W,Other_Prop,Prop1)
  154.           & ~equiv(W,Other_Prop,Prop2)))))
  155.  
  156. exactly_N_lits(N,W) <=>
  157.    range_lits(N,N,W).  
  158.  
  159.  
  160. range_lits(N,M,W) <=>
  161.  exists(W,
  162.   ( min_lits(N,W)
  163.     & max_lits(M,W))) .
  164.  
  165. min_lits(1,W) <=>
  166.  exists([W,Prop],
  167.      (true_in_world(Prop,W))).
  168.  
  169. min_lits(2,W) <=>
  170.  exists([W,Prop1,Prop2],
  171.    (  true_in_world(Prop1,W)
  172.     & true_in_world(Prop2,W)
  173.     & ~equiv(W,Prop1,Prop2))).
  174.  
  175. max_lits(2,W) <=>  
  176. exists([W,Prop1,Prop2],
  177.    (  true_in_world(Prop1,W)
  178.     & true_in_world(Prop2,W)
  179.     &  ~exists(Other_Prop,
  180.           (  true_in_world(Other_Prop,W)
  181.             & ~equiv(W,Other_Prop,Prop1)
  182.             & ~equiv(W,Other_Prop,Prop2))))).
  183.  
  184. % exists a W with no lits?
  185. exactly_N_lits(0,W) <=>
  186.   exists(W,
  187.      ~exists(Prop1, true_in_world(Prop1,W))).
  188.  
  189. max_lits(1,W) <=>
  190.  exactly_N_lits(0,W) v exactly_N_lits(1,W).
  191.  
  192. difference_at_least_1_truths(W1,W2) <=>
  193.   exists(Prop, (true_in_world(Prop,W1) => ~true_in_world(Prop,W2))) .
  194.  
  195. disjoint_truths(W1,W2) <=>
  196.   ~exists(Prop, (true_in_world(Prop,W1) & true_in_world(Prop,W2))).
  197.  
  198. subset_truths(W1,W2) <=>
  199.     all(Prop,
  200.       true_in_world(Prop,W1) => true_in_world(Prop,W2) ).
  201.  
  202. union_s_v2(W1,W2,W) <=>
  203.  all(Prop,
  204.    (true_in_world(Prop,W) <=>
  205.        (true_in_world(Prop,W1) v true_in_world(Prop,W2)))).
  206.  
  207. union_truths(W1,W2,W) <=>
  208.   exists(KB,
  209.       union_truths(W1,W2,KB)
  210.      & ~difference_at_least_1_truths(W,KB)).
  211.  
  212.  
  213. union_disjoint_truths(W1,W2,W) <=>
  214.    (   union_truths(W1,W2,W)
  215.      & disjoint_truths(W1,W2)).
  216.  
  217.  
  218. min_lits(4,W) <=>
  219.   exists([W1,W2],
  220.      min_lits(2,W1)
  221.    & min_lits(2,W2)
  222.    & union_disjoint_truths(W1,W2)).
  223.  
  224. min_lits(N,W) <=>
  225.   exists([W1,W2],
  226.      min_lits(1,W1)
  227.    & min_lits(M,W2)
  228.    & consistent(W2)
  229.    & union_disjoint_truths(W1,W2)
  230.    & my_minus_one(N,M)).
  231.  
  232.  
  233. max_lits(N,W) <=>
  234.   exists([W1,W2],
  235.      max_lits(1,W1)
  236.    & max_lits(M,W2)
  237.    & consistent(W2)
  238.    & union_disjoint_truths(W1,W2)
  239.    & my_minus_one(N,M)).
  240.  
  241.  
  242. equal_v1_truths(W1,W2) <=>
  243.    ( ~difference_at_least_1_truths(W1,W2)
  244.      & ~difference_at_least_1_truths(W2,W1)
  245.      & consistent(W1)
  246.      & consistent(W2)).
  247.  
  248. equal_v2_truths(W1,W2) <=>
  249.  ( consistent(W1)
  250.    & all(Prop,
  251.       (true_in_world(Prop,W1) <=> true_in_world(Prop,W2)))).
  252.  
  253.  
  254. % v1: lameness
  255. equiv_v1(W,Prop1,Prop2) <=>
  256.   true_in_world(Prop1,W) <=>   true_in_world(Prop2,W).
  257.  
  258. % v2  Prop2 and Prop2 logically "imply" each other in the W.
  259. equiv_v2(W,Prop1,Prop2) <=>
  260.   true_in_world((Prop1 <=> Prop2),W).
  261.  
  262. % v3 the actual semantics implemented based that both logical sentences use the same proof
  263. equiv(W,Prop1,Prop2) <=>
  264.   equiv_v4(W,Prop1,Prop2) v equiv_v2(W,Prop1,Prop2).
  265.  
  266. % v4 sameness (current implementation in LogicMOO )
  267. equiv_v4(W,X,Y) <=>
  268.  same(X,Y) &
  269.  forall(X,
  270.   exists(W,
  271.    true_in_world(X,W))).
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!