View difference between Paste ID: H5W1TFq6 and rzW9KkPC

 
-#import: written-on(word,paper).
+
 my-minus-one(N,M) <->  (N > 1)  &  (M = N-1)
 
 % Lits in KBs are considered true
 consistent(kb) <-> min-lits(1, kb)
-forall x. same(x,x)
+
 exactly-N-lits(1,kb) <->
-legal-pad(paper) <-> min-elements(1, paper)
+(exists kb logsent.
     (   true-in(logsent,kb)
-exactly-n-elements(1,paper) <->
+      & ~(exists other-logsent.
-(exists paper word.
+           (  true-in(other-logsent,kb)
-    (   written-on(word,paper)
+             & ~equiv(kb,other-logsent,logsent)))))
-      & ~(exists other-word.
+
-           (  written-on(other-word,paper)
+exactly-N-lits(2,kb) <->
-             & ~same(other-word,word)))))
+(exists kb logsent1 logsent2.
   (  true-in(logsent1,kb)
-exactly-n-elements(2,paper) <->
+   & true-in(logsent2,kb)
-(exists paper word1 word2.
+   & ~equiv(kb,logsent1,logsent2)
-  (  written-on(word1,paper)
+   & ~ (exists other-logsent.
-   & written-on(word2,paper)
+         (  true-in(other-logsent,kb)
-   & ~same(word1,word2)
+          & ~equiv(kb,other-logsent,logsent1)
-   & ~ (exists other-word.
+          & ~equiv(kb,other-logsent,logsent2)))))
-         (   written-on(other-word,paper)
+
-          & ~same(other-word,word1)
+exactly-N-lits(N,kb) <->
-          & ~same(other-word,word2)))))
+   range-lits(N,N,kb)
 
-exactly-n-elements(N,paper) <->
+
-   range-elements(N,N,paper)
+range-lits(N,M,kb) <->
  (exists kb.
-range-elements(N,M,paper) <->
+  ( min-lits(N,kb)
- (exists paper.
+    & max-lits(M,kb)))
-  ( min-elements(N,paper)
+
-    & max-elements(M,paper)))
+min-lits(1,kb) <->
  (exists kb logsent1.
-min-elements(1,paper) <->
+     (true-in(logsent1,kb)))
- (exists paper word1.
+
-     (written-on(word1,paper)))
+min-lits(2,kb) <->
  (exists kb logsent1 logsent2.
-min-elements(2,paper) <->
+   (  true-in(logsent1,kb)
- (exists paper word1 word2.
+    & true-in(logsent2,kb)
-   (  written-on(word1,paper)
+    & ~equiv(kb,logsent1,logsent2)))
-    & written-on(word2,paper)
+
-    & ~same(word1,word2)))
+max-lits(2,kb) <->
 (exists kb logsent1 logsent2.
-max-elements(2,paper) <->
+   (  true-in(logsent1,kb)
-(exists paper word1 word2.
+    & true-in(logsent2,kb)
-   (  written-on(word1,paper)
+    &  ~(exists other-logsent.
-    & written-on(word2,paper)
+          (  true-in(other-logsent,kb)
-    &  ~(exists other-word.
+            & ~equiv(kb,other-logsent,logsent1)
-          (  written-on(other-word,paper)
+            & ~equiv(kb,other-logsent,logsent2)))))
-            & ~same(other-word,word1)
+
-            & ~same(other-word,word2)))))
+% exists a kb with no lits?
 exactly-N-lits(0,kb) <->
-% exists a paper with no elements
+  (exists kb
-exactly-n-elements(0,paper) <->
+     ~(exists logsent1. true-in(logsent1,kb)))
-  (exists paper
+
-     ~(exists word1. written-on(word1,paper)))
+max-lits(1,kb) <->
  exactly-N-lits(0,kb) v exactly-N-lits(1,kb)
-max-elements(1,paper) <->
+
- exactly-n-elements(0,paper) v exactly-n-elements(1,paper)
+difference_at_least_1_truths(kb1,kb2) <->
   (exists logsent. (true-in(logsent,kb1) -> ~true-in(logsent,kb2)))
-containsAtLeastOneUnique(paper1,paper2) <->
+
-  (exists word. (written-on(word,paper1) -> ~written-on(word,paper2)))
+disjoint_truths(kb1,kb2) <->
   ~(exists logsent. (true-in(logsent,kb1) & true-in(logsent,kb2)))
-disjoint(paper1,paper2) <->
+
-  ~(exists word. (written-on(word,paper1) & written-on(word,paper2)))
+subset_truths(kb1,kb2) <->
     (forall logsent.
-subset(paper1,paper2) <->
+      true-in(logsent,kb1) -> true-in(logsent,kb2) )
-    (forall word.
+
-      written-on(word,paper1) -> written-on(word,paper2) )
+union_s_v2(kb1,kb2,kb) <->
  (forall logsent.
-union(paper1,paper2,paper) <->
+   (true-in(logsent,kb) <->
- (forall word.
+       (true-in(logsent,kb1) v true-in(logsent,kb2))))
-   (written-on(word,paper) <->
+
-       (written-on(word,paper1) v written-on(word,paper2))))
+union_truths(kb1,kb2,kb) <->
   (exists scratchpad.
-union(paper1,paper2,paper) <->
+      union_truths(kb1,kb2,scratchpad)
      & ~difference_at_least_1_truths(kb,scratchpad))
-      union(paper1,paper2,scratchpad)
+
-     & ~containsAtLeastOneUnique(paper,scratchpad))
+
 union-disjoint_truths(kb1,kb2,kb) <->
    (   union_truths(kb1,kb2,kb)
-union-disjoint(paper1,paper2,paper) <->
+     & disjoint_truths(kb1,kb2))
-   (   union(paper1,paper2,paper)
+
-     & disjoint(paper1,paper2))
+
 min-lits(4,kb) <->
   (exists kb1 kb2.
-min-elements(4,paper) <->
+     min-lits(2,kb1)
-  (exists paper1 paper2.
+   & min-lits(2,kb2)
-     min-elements(2,paper1)
+   & union-disjoint_truths(kb1,kb2))
-   & min-elements(2,paper2)
+
-   & union-disjoint(paper1,paper2))
+min-lits(N,kb) <->
   (exists kb1 kb2.
-min-elements(N,paper) <->
+     min-lits(1,kb1)
-  (exists paper1 paper2.
+   & min-lits(M,kb2)
-     min-elements(1,paper1)
+   & consistent(kb2)
-   & min-elements(M,paper2)
+   & union-disjoint_truths(kb1,kb2)
-   & legal-pad(paper2)
+
-   & union-disjoint(paper1,paper2)
+
 
 max-lits(N,kb) <->
   (exists kb1 kb2.
-max-elements(N,paper) <->
+     max-lits(1,kb1)
-  (exists paper1 paper2.
+   & max-lits(M,kb2)
-     max-elements(1,paper1)
+   & consistent(kb2)
-   & max-elements(M,paper2)
+   & union-disjoint_truths(kb1,kb2)
-   & legal-pad(paper2)
+
-   & union-disjoint(paper1,paper2)
+
 
 equal_v1_truths(kb1,kb2) <->
    ( ~difference_at_least_1_truths(kb1,kb2)
-equal_papers_v2(paper1,paper2) <->
+     & ~difference_at_least_1_truths(kb2,kb1)
-   ( ~containsAtLeastOneUnique(paper1,paper2)
+     & consistent(kb1)
-     & ~containsAtLeastOneUnique(paper2,paper1)
+     & consistent(kb2))
-     & legal-pad(paper1)
+
-     & legal-pad(paper2))
+equal_v2_truths(kb1,kb2) <->
  ( consistent(kb1)
-equal_papers_v1(paper1,paper2) <->
+   & (forall logsent.
- ( legal-pad(paper1)
+      (true-in(logsent,kb1) <-> true-in(logsent,kb2))))
-   & (forall word.
+
-      (written-on(word,paper1) <-> written-on(word,paper2))))
+
 % v1: lameness
 equiv_v1(kb,logsent1,logsent2) <->
   true-in(logsent1,kb) <->   true-in(logsent2,kb)
 
 % v2  logsent2 and logsent2 logically "imply" each other in the kb.
 equiv_v2(kb,logsent1,logsent2) <->
   true-in((logsent1 <-> logsent2),kb)
 
 % v3 the actual semantics implemented based that both logical sentences use the same proof
 equiv(kb,logsent1,logsent2) <->
   equiv_v4(kb,logsent1,logsent2) v equiv_v2(kb,logsent1,logsent2)
 
 % v4 sameness (current implementation in LogicMOO )
 equiv_v4(kb,x,x) <->
  (forall x. (exists kb.
   true-in(x,kb)))