ideas about lists and list inferences

tests/Lists.kif

@@ -0,0 +1,57 @@
+; Lists.kif
+(instance Chad Organism)
+(instance Adam Organism)
+(not (equal Chad Adam))
+(instance ChadsOffice GeographicArea)
+(instance inhabits BinaryPredicate)
+(domain inhabits 1 Object)
+(domain inhabits 2 Physical)
+
+(<=>
+  (instance ?I ?C)
+  (inList ?I 
+    (ClassToListFn ?C)))
+
+(instance ClassToListFn UnaryFunction)
+(domain ClassToListFn 1 Class)
+(range ClassToListFn List)
+
+(domain CardinalityFn 1 Class)
+(instance CardinalityFn UnaryFunction)	
+(range CardinalityFn Integer)
+
+(equal
+  (CardinalityFn ?C)
+  (ListLengthFn 
+    (ClassToListFn ?C)))
+
+(=>
+  (instance ?X ?C)
+  (not
+    (equal 0 (CardinalityFn (ClassToListFn ?C)))))
+
+(=>
+  (and
+    (instance ?X ?C)
+    (not
+      (instance ?X2 ?C))
+    (not
+      (equal ?X ?X2)))
+  (equal 1 
+    (CardinalityFn 
+      (ClassToListFn ?C))))
+
+(instance MyList List)
+(equal MyList (ListFn Adam Chad))
+
+; queries    
+; (inList Chad (ClassToListFn Organism)) - works
+; (equal 2 (ListLengthFn (ClassToListFn Organism))) - works maybe - why does proof use MyList?
+; (equal 2 (CardinalityFn Organism)) - fail
+; (equal (ListFn Adam Chad) (ClassToListFn Organism)) - works
+; (and (instance ?X Organism) (not (equal ?X Chad))) - works
+; (equal 2 (ListLengthFn MyList)) - works
+; (equal Adam (FirstFn MyList)) - works
+; (equal (ListFn Adam) (SubListFn 1 2 MyList)) - works
+; (equal 2 (ListLengthFn (SubListFn 1 3 MyList))) - works
+