forked from ontologyportal/sumo
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathMerge.kif
executable file
·17237 lines (14138 loc) · 567 KB
/
Merge.kif
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
;; ================================================
;; SUMO (Suggested Upper Merged Ontology)
;; ================================================
;; The original versions of SUMO incorporated elements from many public sources
;; which are documented at http://www.ontologyportal.org/SUMOhistory/
;; The SUMO is freely available, subject to the following IEEE license.
;; ----------------------
;; Copyright � 2004 by the Institute of Electrical and Electronics Engineers, Inc.
;; Three Park Avenue
;; New York, NY 10016-5997, USA
;; All rights reserved.
;; 1. COPYRIGHT
;; The Institute of Electrical and Electronics Engineers, Inc., ("IEEE") owns the
;; copyright to this Document in all forms of media. Copyright in the text retrieved,
;; displayed or output from this Document is owned by IEEE and is protected by the
;; copyright laws of the United States and by international treaties. The IEEE reserves
;; all rights not expressly granted herein.
;; 2. ROYALTIES
;; The IEEE is providing the Document at no charge. However, the Document is not to be
;; considered "Public Domain," as the IEEE is, and at all times shall remain, the sole
;; copyright holder in the Document. The IEEE intends to revise the Document from time to
;; time; the latest version shall be available at http://standards.ieee.org/catalog/
;; 3. TERMS OF USE
;; The IEEE hereby grants Licensee a perpetual, non-exclusive, royalty-free, world-wide
;; right and license to copy, publish and distribute the Document in any way, and to
;; prepare derivative works that are based on or incorporate all or part of the Document
;; provided that the IEEE is appropriately acknowledged as the source and copyright owner
;; in each and every use.
;; 4. LIMITED WARRANTIES & LIMITATIONS OF REMEDIES
;; LICENSOR Does not warrant or represent the accuracy or content of the document and
;; Expressly Disclaims any Express or Implied Warranty, including any Implied Warranty of
;; Merchantability or Fitness for a Specific Purpose or that the use of the document is
;; free from patent infringement. The document is supplied ONLY "AS IS."
;; ----------------------
;; The SUMO was initially developed at Teknowledge Corp.
;; Any questions or comments about this ontology can be directed to the
;; Technical editor, Adam Pease, apease [at] articulatesoftware [dot] com
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; The knowledge representation language in which the SUMO is expressed is SUO-KIF,
;; which stands for "Standard Upper Ontology - Knowledge Interchange Format". SUO-KIF
;; is a simplified form of the popular KIF knowledge representation language. A
;; specification of SUO-KIF can be found at: http://www.ontologyportal.org
;; The SUMO is a modular ontology. That is, the ontology is divided into
;; self-contained subontologies. Each subontology is indicated by a section
;; header, and the dependencies between the subontologies are specified with
;; statements of the form ";; INCLUDES '<SUBONTOLOGY>'". These statements are
;; found at the beginning of each section.
;; We ask the people using or referencing SUMO cite our primary paper:
;; Niles, I., and Pease, A. 2001. Towards a Standard Upper Ontology. In
;; Proceedings of the 2nd International Conference on Formal Ontology in
;; Information Systems (FOIS-2001), Chris Welty and Barry Smith, eds,
;; Ogunquit, Maine, October 17-19, 2001. Also see http://www.ontologyportal.org
;; BEGIN FILE
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; STRUCTURAL ONTOLOGY ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; INCLUDES 'BASE ONTOLOGY'
;; The Structural Ontology consists of definitions of certain syntactic
;; abbreviations that can be both heuristically useful and computationally
;; advantageous.
(instance instance BinaryPredicate)
(domain instance 1 Entity)
(domain instance 2 Class)
(documentation instance EnglishLanguage "An object is an &%instance of a &%Class if
it is included in that &%Class. An individual may be an &%instance of many
classes, some of which may be subclasses of others. Thus, there is no
assumption in the meaning of &%instance about specificity or uniqueness.")
(subrelation immediateInstance instance)
(instance immediateInstance AsymmetricRelation)
(instance immediateInstance IntransitiveRelation)
(documentation immediateInstance EnglishLanguage "An object is an &%immediateInstance of
a &%Class if it is an &%instance of the &%Class and it is not an
&%instance of a proper subclass of &%Class.")
(=>
(immediateInstance ?ENTITY ?CLASS)
(not (exists (?SUBCLASS)
(and
(subclass ?SUBCLASS ?CLASS)
(not (equal ?SUBCLASS ?CLASS))
(instance ?ENTITY ?SUBCLASS)))))
(instance inverse BinaryPredicate)
(instance inverse IrreflexiveRelation)
(instance inverse IntransitiveRelation)
(instance inverse SymmetricRelation)
(instance inverse PartialValuedRelation)
(domain inverse 1 BinaryRelation)
(domain inverse 2 BinaryRelation)
(documentation inverse EnglishLanguage "The inverse of a &%BinaryRelation is a &%Relation
in which all the tuples of the original &%Relation are reversed. In other words, one
&%BinaryRelation is the inverse of another if they are equivalent when their arguments
are swapped.")
; causes a predicate variable expansion explosion
; (=>
; (and
; (inverse ?REL1 ?REL2)
; (instance ?REL1 Predicate)
; (instance ?REL2 Predicate))
; (forall (?INST1 ?INST2)
; (<=>
; (?REL1 ?INST1 ?INST2)
; (?REL2 ?INST2 ?INST1))))
(instance subclass BinaryPredicate)
(instance subclass PartialOrderingRelation)
(domain subclass 1 Class)
(domain subclass 2 Class)
(documentation subclass EnglishLanguage "(&%subclass ?CLASS1 ?CLASS2) means that ?CLASS1
is a &%subclass of ?CLASS2, i.e. every &%instance of ?CLASS1 is also an &%instance of
?CLASS2. A &%Class may have multiple superclasses and subclasses.")
(=>
(subclass ?X ?Y)
(and
(instance ?X Class)
(instance ?Y Class)))
(=>
(and
(subclass ?X ?Y)
(instance ?Z ?X))
(instance ?Z ?Y))
; (subrelation immediateSubclass subclass)
(instance immediateSubclass AsymmetricRelation)
(instance immediateSubclass IntransitiveRelation)
(instance immediateSubclass BinaryPredicate)
(domain immediateSubclass 1 Class)
(domain immediateSubclass 2 Class)
(documentation immediateSubclass EnglishLanguage "A &%Class ?CLASS1 is an
&%immediateSubclass of another &%Class ?CLASS2 just in case ?CLASS1 is a subclass of
?CLASS2 and there is no other subclass of ?CLASS2 such that ?CLASS1 is also a subclass of
it.")
(=>
(immediateSubclass ?CLASS1 ?CLASS2)
(not (exists (?CLASS3)
(and
(subclass ?CLASS3 ?CLASS2)
(subclass ?CLASS1 ?CLASS3)
(not (equal ?CLASS2 ?CLASS3))
(not (equal ?CLASS1 ?CLASS3))))))
(instance subrelation BinaryPredicate)
(instance subrelation PartialOrderingRelation)
(domain subrelation 1 Relation)
(domain subrelation 2 Relation)
(documentation subrelation EnglishLanguage "(&%subrelation ?REL1 ?REL2) means that
every tuple of ?REL1 is also a tuple of ?REL2. In other words, if
the &%Relation ?REL1 holds for some arguments arg_1, arg_2, ... arg_n,
then the &%Relation ?REL2 holds for the same arguments. A consequence
of this is that a &%Relation and its subrelations must have the same
&%valence.")
(=>
(and
(subrelation ?PRED1 ?PRED2)
(valence ?PRED1 ?NUMBER))
(valence ?PRED2 ?NUMBER))
(=>
(and
(subrelation ?PRED1 ?PRED2)
(domain ?PRED2 ?NUMBER ?CLASS1))
(domain ?PRED1 ?NUMBER ?CLASS1))
(=>
(and
(subrelation ?REL1 ?REL2)
(instance ?REL1 Predicate)
(instance ?REL2 Predicate)
(?REL1 @ROW))
(?REL2 @ROW))
(=>
(and
(subrelation ?PRED1 ?PRED2)
(instance ?PRED2 ?CLASS)
(subclass ?CLASS InheritableRelation))
(instance ?PRED1 ?CLASS))
(instance domain TernaryPredicate)
(domain domain 1 Relation)
(domain domain 2 PositiveInteger)
(domain domain 3 Class)
(documentation domain EnglishLanguage "Provides a computationally and heuristically
convenient mechanism for declaring the argument types of a given relation.
The formula (&%domain ?REL ?INT ?CLASS) means that the ?INT'th element of each
tuple in the relation ?REL must be an instance of ?CLASS. Specifying argument
types is very helpful in maintaining ontologies. Representation systems can
use these specifications to classify terms and check integrity constraints.
If the restriction on the argument type of a &%Relation is not captured by a
&%Class already defined in the ontology, one can specify a &%Class
compositionally with the functions &%UnionFn, &%IntersectionFn, etc.")
(=>
(and
(domain ?REL ?NUMBER ?CLASS1)
(domain ?REL ?NUMBER ?CLASS2))
(or
(subclass ?CLASS1 ?CLASS2)
(subclass ?CLASS2 ?CLASS1)))
(instance domainSubclass TernaryPredicate)
(domain domainSubclass 1 Relation)
(domain domainSubclass 2 PositiveInteger)
(domain domainSubclass 3 Class)
(documentation domainSubclass EnglishLanguage "A &%Predicate that is used to specify
argument type restrictions of &%Predicates. The formula (&%domainSubclass
?REL ?INT ?CLASS) means that the ?INT'th element of each tuple in the
relation ?REL must be a subclass of ?CLASS.")
(=>
(and
(subrelation ?REL1 ?REL2)
(domainSubclass ?REL2 ?NUMBER ?CLASS1))
(domainSubclass ?REL1 ?NUMBER ?CLASS1))
(=>
(and
(domainSubclass ?REL ?NUMBER ?CLASS1)
(domainSubclass ?REL ?NUMBER ?CLASS2))
(or
(subclass ?CLASS1 ?CLASS2)
(subclass ?CLASS2 ?CLASS1)))
;(instance equal BinaryPredicate)
;(instance equal EquivalenceRelation)
;(instance equal RelationExtendedToQuantities)
;(domain equal 1 Entity)
;(domain equal 2 Entity)
;(documentation equal EnglishLanguage "(equal ?ENTITY1 ?ENTITY2) is true just in case
;?ENTITY1 is identical with ?ENTITY2.")
(=>
(equal ?THING1 ?THING2)
(forall (?ATTR)
(<=>
(property ?THING1 ?ATTR)
(property ?THING2 ?ATTR))))
(=>
(equal ?ATTR1 ?ATTR2)
(forall (?THING)
(<=>
(property ?THING ?ATTR1)
(property ?THING ?ATTR2))))
(=>
(equal ?THING1 ?THING2)
(forall (?CLASS)
(<=>
(instance ?THING1 ?CLASS)
(instance ?THING2 ?CLASS))))
(=>
(equal ?CLASS1 ?CLASS2)
(forall (?THING)
(<=>
(instance ?THING ?CLASS1)
(instance ?THING ?CLASS2))))
;;(=>
;; (equal ?REL1 ?REL2)
;; (forall (@ROW)
;; (<=>
;; (?REL1 @ROW)
;; (?REL2 @ROW))))
(=>
(equal ?LIST1 ?LIST2)
(=>
(and
(equal ?LIST1 (ListFn @ROW1))
(equal ?LIST2 (ListFn @ROW2)))
(forall (?NUMBER)
(equal (ListOrderFn (ListFn @ROW1) ?NUMBER) (ListOrderFn (ListFn @ROW2) ?NUMBER)))))
(instance range BinaryPredicate)
(instance range AsymmetricRelation)
(domain range 1 Function)
(domain range 2 Class)
(documentation range EnglishLanguage "Gives the range of a function. In other words,
(&%range ?FUNCTION ?CLASS) means that all of the values assigned by
?FUNCTION are &%instances of ?CLASS.")
(=>
(and
(range ?FUNCTION ?CLASS)
(equal (AssignmentFn ?FUNCTION @ROW) ?VALUE))
(instance ?VALUE ?CLASS))
(=>
(and
(subrelation ?REL1 ?REL2)
(range ?REL2 ?CLASS1))
(range ?REL1 ?CLASS1))
(=>
(and
(range ?REL ?CLASS1)
(range ?REL ?CLASS2))
(or
(subclass ?CLASS1 ?CLASS2)
(subclass ?CLASS2 ?CLASS1)))
(instance rangeSubclass BinaryPredicate)
(instance rangeSubclass AsymmetricRelation)
(domain rangeSubclass 1 Function)
(domainSubclass rangeSubclass 2 Class)
(documentation rangeSubclass EnglishLanguage "(&%rangeSubclass ?FUNCTION ?CLASS) means
that all of the values assigned by ?FUNCTION are &%subclasses of ?CLASS.")
(=>
(and
(rangeSubclass ?FUNCTION ?CLASS)
(equal (AssignmentFn ?FUNCTION @ROW) ?VALUE))
(subclass ?VALUE ?CLASS))
(=>
(and
(subrelation ?REL1 ?REL2)
(rangeSubclass ?REL2 ?CLASS1))
(rangeSubclass ?REL1 ?CLASS1))
(=>
(and
(rangeSubclass ?REL ?CLASS1)
(rangeSubclass ?REL ?CLASS2))
(or
(subclass ?CLASS1 ?CLASS2)
(subclass ?CLASS2 ?CLASS1)))
(instance valence BinaryPredicate)
(instance valence AsymmetricRelation)
(instance valence SingleValuedRelation)
(domain valence 1 Relation)
(domain valence 2 PositiveInteger)
(documentation valence EnglishLanguage "Specifies the number of arguments that a
relation can take. If a relation does not have a fixed number of
arguments, it does not have a valence and it is an instance of
&%VariableArityRelation.")
(instance documentation TernaryPredicate)
(domain documentation 1 Entity)
(domain documentation 2 HumanLanguage)
(domain documentation 3 SymbolicString)
(documentation documentation EnglishLanguage "A relation between objects
in the domain of discourse and strings of natural language text stated in
a particular &%HumanLanguage. The domain of &%documentation is not
constants (names), but the objects themselves. This means that one does
not quote the names when associating them with their documentation.")
(instance format TernaryPredicate)
(domain format 1 Language)
(domain format 2 Entity)
(domain format 3 SymbolicString)
(documentation format EnglishLanguage "A relation that specifies how
to present an expression in a natural language format.")
(instance termFormat TernaryPredicate)
(domain termFormat 1 Language)
(domain termFormat 2 Entity)
(domain termFormat 3 SymbolicString)
(documentation termFormat EnglishLanguage "A relation that specifies how
to present a term in a natural language format.")
(instance disjoint BinaryPredicate)
(instance disjoint SymmetricRelation)
(domain disjoint 1 Class)
(domain disjoint 2 Class)
(documentation disjoint EnglishLanguage "&%Classes are &%disjoint only if they share no
instances, i.e. just in case the result of applying &%IntersectionFn to
them is empty.")
(=>
(disjoint ?CLASS1 ?CLASS2)
(forall (?INST)
(not
(and
(instance ?INST ?CLASS1)
(instance ?INST ?CLASS2)))))
(instance disjointRelation BinaryPredicate)
(instance disjointRelation IrreflexiveRelation)
(instance disjointRelation PartialValuedRelation)
(domain disjointRelation 1 Relation)
(domain disjointRelation 2 Relation)
(relatedInternalConcept disjointRelation disjoint)
(documentation disjointRelation EnglishLanguage "This predicate relates two &%Relations.
(&%disjointRelation ?REL1 ?REL2) means that the two relations have no tuples in
common.")
(=>
(and
(domain ?REL1 ?NUMBER ?CLASS1)
(domain ?REL2 ?NUMBER ?CLASS2)
(disjoint ?CLASS1 ?CLASS2))
(disjointRelation ?REL1 ?REL2))
(=>
(and
(domainSubclass ?REL1 ?NUMBER ?CLASS1)
(domainSubclass ?REL2 ?NUMBER ?CLASS2)
(disjoint ?CLASS1 ?CLASS2))
(disjointRelation ?REL1 ?REL2))
(=>
(and
(range ?REL1 ?CLASS1)
(range ?REL2 ?CLASS2)
(disjoint ?CLASS1 ?CLASS2))
(disjointRelation ?REL1 ?REL2))
(=>
(and
(rangeSubclass ?REL1 ?CLASS1)
(rangeSubclass ?REL2 ?CLASS2)
(disjoint ?CLASS1 ?CLASS2))
(disjointRelation ?REL1 ?REL2))
(=>
(and
(instance ?REL1 Predicate)
(instance ?REL2 Predicate)
(disjointRelation ?REL1 ?REL2)
(?REL1 @ROW2))
(not (?REL2 @ROW2)))
(instance contraryAttribute Predicate)
(instance contraryAttribute VariableArityRelation)
(domain contraryAttribute 1 Attribute)
(documentation contraryAttribute EnglishLanguage "A &%contraryAttribute is a set of &%Attributes
such that something can not simultaneously have more than one of these &%Attributes.
For example, (&%contraryAttribute &%Pliable &%Rigid) means that nothing can be both
&%Pliable and &%Rigid.")
(=>
(contraryAttribute @ROW)
(=>
(inList ?ELEMENT (ListFn @ROW))
(instance ?ELEMENT Attribute)))
(=>
(and
(contraryAttribute @ROW1)
(identicalListItems (ListFn @ROW1) (ListFn @ROW2)))
(contraryAttribute @ROW2))
(=>
(contraryAttribute @ROW)
(forall (?ATTR1 ?ATTR2)
(=>
(and
(equal ?ATTR1 (ListOrderFn (ListFn @ROW) ?NUMBER1))
(equal ?ATTR2 (ListOrderFn (ListFn @ROW) ?NUMBER2))
(not (equal ?NUMBER1 ?NUMBER2)))
(=>
(property ?OBJ ?ATTR1)
(not (property ?OBJ ?ATTR2))))))
(instance exhaustiveAttribute Predicate)
(instance exhaustiveAttribute VariableArityRelation)
(domainSubclass exhaustiveAttribute 1 Attribute)
(domain exhaustiveAttribute 2 Attribute)
(documentation exhaustiveAttribute EnglishLanguage "This predicate relates a &%Class to a
set of &%Attributes, and it means that the elements of this set exhaust the
instances of the &%Class. For example, (&%exhaustiveAttribute &%PhysicalState
&%Solid &%Fluid &%Liquid &%Gas &%Plasma) means that there are only five instances of
the class &%PhysicalState, viz. &%Solid, &%Fluid, &%Liquid, &%Gas and &%Plasma.")
(=>
(and
(exhaustiveAttribute ?CLASS @ROW)
(inList ?ATTR (ListFn @ROW)))
(instance ?ATTR Attribute))
(=>
(and
(exhaustiveAttribute ?CLASS @ROW)
(inList ?ATTR (ListFn @ROW)))
(instance ?ATTR ?CLASS))
(=>
(exhaustiveAttribute ?CLASS @ROW)
(forall (?ATTR1)
(=>
(instance ?ATTR1 ?CLASS)
(exists (?ATTR2)
(and
(inList ?ATTR2 (ListFn @ROW))
(equal ?ATTR1 ?ATTR2))))))
(=>
(exhaustiveAttribute ?ATTRCLASS @ROW)
(not
(exists (?EL)
(and
(instance ?EL ?ATTRCLASS)
(not
(exists (?ATTR ?NUMBER)
(and
(equal ?EL ?ATTR)
(equal ?ATTR
(ListOrderFn
(ListFn @ROW) ?NUMBER)))))))))
(=>
(exhaustiveAttribute ?CLASS @ROW)
(=>
(equal ?ATTR1
(ListOrderFn (ListFn @ROW) ?N1))
(not
(exists (?ATTR2 ?N2)
(and
(equal ?ATTR1 ?ATTR2)
(not
(equal ?N1 ?N2)))))))
(instance exhaustiveDecomposition Predicate)
(instance exhaustiveDecomposition VariableArityRelation)
(domain exhaustiveDecomposition 1 Class)
(domain exhaustiveDecomposition 2 Class)
(relatedInternalConcept exhaustiveDecomposition partition)
(documentation exhaustiveDecomposition EnglishLanguage "An &%exhaustiveDecomposition of a
&%Class C is a set of subclasses of C such that every instance of C is an
instance of one of the subclasses in the set. Note: this does not necessarily
mean that the elements of the set are disjoint (see &%partition - a &%partition
is a disjoint exhaustive decomposition).")
(=>
(exhaustiveDecomposition @ROW)
(=>
(inList ?ELEMENT (ListFn @ROW))
(instance ?ELEMENT Class)))
(instance disjointDecomposition Predicate)
(instance disjointDecomposition VariableArityRelation)
(domain disjointDecomposition 1 Class)
(domain disjointDecomposition 2 Class)
(relatedInternalConcept disjointDecomposition exhaustiveDecomposition)
(relatedInternalConcept disjointDecomposition disjoint)
(documentation disjointDecomposition EnglishLanguage "A &%disjointDecomposition of a
&%Class C is a set of subclasses of C that are mutually &%disjoint.")
(=>
(disjointDecomposition @ROW)
(=>
(inList ?ELEMENT (ListFn @ROW))
(instance ?ELEMENT Class)))
(instance partition Predicate)
(instance partition VariableArityRelation)
(domain partition 1 Class)
(domain partition 2 Class)
(documentation partition EnglishLanguage "A &%partition of a &%Class C
is a set of mutually &%disjoint classes (a subclass partition) which
covers C. Every instance of C is an instance of exactly one of the
subclasses in the partition.")
(<=>
(partition @ROW)
(and
(exhaustiveDecomposition @ROW)
(disjointDecomposition @ROW)))
(instance relatedInternalConcept BinaryPredicate)
(instance relatedInternalConcept EquivalenceRelation)
(domain relatedInternalConcept 1 Entity)
(domain relatedInternalConcept 2 Entity)
(documentation relatedInternalConcept EnglishLanguage "Means that the two arguments are
related concepts within the SUMO, i.e. there is a significant similarity
of meaning between them. To indicate a meaning relation between a SUMO
concept and a concept from another source, use the Predicate
&%relatedExternalConcept.")
(instance relatedExternalConcept TernaryPredicate)
(domain relatedExternalConcept 1 SymbolicString)
(domain relatedExternalConcept 2 Entity)
(domain relatedExternalConcept 3 Language)
(relatedInternalConcept relatedExternalConcept relatedInternalConcept)
(documentation relatedExternalConcept EnglishLanguage "Used to signify a three-place
relation between a concept in an external knowledge source, a concept
in the SUMO, and the name of the other knowledge source.")
(subrelation synonymousExternalConcept relatedExternalConcept)
(instance synonymousExternalConcept TernaryPredicate)
(disjointRelation synonymousExternalConcept subsumedExternalConcept)
(disjointRelation synonymousExternalConcept subsumingExternalConcept)
(disjointRelation subsumedExternalConcept subsumingExternalConcept)
(documentation synonymousExternalConcept EnglishLanguage "(&%synonymousExternalConcept
?STRING ?THING ?LANGUAGE) means that the SUMO concept ?THING has the
same meaning as ?STRING in ?LANGUAGE.")
(subrelation subsumingExternalConcept relatedExternalConcept)
(instance subsumingExternalConcept TernaryPredicate)
(documentation subsumingExternalConcept EnglishLanguage "(&%subsumingExternalConcept
?STRING ?THING ?LANGUAGE) means that the SUMO concept ?THING subsumes
the meaning of ?STRING in ?LANGUAGE, i.e. the concept ?THING is broader
in meaning than ?STRING.")
(subrelation subsumedExternalConcept relatedExternalConcept)
(instance subsumedExternalConcept TernaryPredicate)
(documentation subsumedExternalConcept EnglishLanguage "(&%subsumedExternalConcept
?STRING ?THING ?LANGUAGE) means that the SUMO concept ?THING is subsumed
by the meaning of ?STRING in ?LANGUAGE, i.e. the concept ?THING is narrower
in meaning than ?STRING.")
(instance externalImage BinaryPredicate)
(documentation externalImage EnglishLanguage "A link between an Entity and a
URL that represents or exemplifies the term in some way.")
(domain externalImage 1 Entity)
(domain externalImage 2 SymbolicString)
(instance subAttribute BinaryPredicate)
(instance subAttribute PartialOrderingRelation)
(domain subAttribute 1 Attribute)
(domain subAttribute 2 Attribute)
(disjointRelation subAttribute successorAttribute)
(documentation subAttribute EnglishLanguage "Means that the second argument can be
ascribed to everything which has the first argument ascribed to it.")
(=>
(subAttribute ?ATTR1 ?ATTR2)
(forall (?OBJ)
(=>
(property ?OBJ ?ATTR1)
(property ?OBJ ?ATTR2))))
(=>
(and
(subAttribute ?ATTR1 ?ATTR2)
(instance ?ATTR2 ?CLASS))
(instance ?ATTR1 ?CLASS))
(instance successorAttribute BinaryPredicate)
(instance successorAttribute AsymmetricRelation)
(domain successorAttribute 1 Attribute)
(domain successorAttribute 2 Attribute)
(documentation successorAttribute EnglishLanguage "(&%successorAttribute ?ATTR1 ?ATTR2)
means that ?ATTR2 is the &%Attribute that comes immediately after ?ATTR1
on the scale that they share.")
(=>
(and
(successorAttribute ?ATTR1 ?ATTR2)
(holdsDuring ?TIME1 (property ?ENTITY ?ATTR2)))
(exists (?TIME2)
(and
(temporalPart ?TIME2 (PastFn ?TIME1))
(holdsDuring ?TIME2 (property ?ENTITY ?ATTR1)))))
(instance successorAttributeClosure BinaryPredicate)
(instance successorAttributeClosure TransitiveRelation)
(instance successorAttributeClosure IrreflexiveRelation)
(instance successorAttributeClosure PartialValuedRelation)
(domain successorAttributeClosure 1 Attribute)
(domain successorAttributeClosure 2 Attribute)
(relatedInternalConcept successorAttributeClosure successorAttribute)
(documentation successorAttributeClosure EnglishLanguage "The transitive closure of
&%successorAttribute. (&%successorAttributeClosure ?ATTR1 ?ATTR2) means
that there is a chain of &%successorAttribute assertions connecting
?ATTR1 and ?ATTR2.")
(=>
(successorAttribute ?ATTR1 ?ATTR2)
(successorAttributeClosure ?ATTR1 ?ATTR2))
(instance greaterThanByQuality TernaryPredicate)
(documentation greaterThanByQuality EnglishLanguage "(greaterThanByQuality
?ENTITY1 ?ENTITY2 ?ATT) means that ?ENTITY1 has more of the given
quality ?ATT than ?ENTITY2.")
(domain greaterThanByQuality 1 Entity)
(domain greaterThanByQuality 2 Entity)
(domain greaterThanByQuality 3 Attribute)
(=>
(and
(greaterThanByQuality ?E1 ?E2 ?ATT)
(greaterThanByQuality ?E2 ?E3 ?ATT))
(greaterThanByQuality ?E1 ?E3 ?ATT))
(=>
(greaterThanByQuality ?E1 ?E2 ?ATT)
(not
(greaterThanByQuality ?E2 ?E1 ?ATT)))
(=>
(greaterThanByQuality ?E1 ?E2 ?ATT)
(not
(equal ?E2 ?E1)))
(instance entails BinaryPredicate)
(domain entails 1 Formula)
(domain entails 2 Formula)
(documentation entails EnglishLanguage "The operator of logical entailment. (&%entails
?FORMULA1 ?FORMULA2) means that ?FORMULA2 can be derived from ?FORMULA1
by means of the proof theory of SUO-KIF.")
;; The following axiom is commented out, because it is rejected by the
;; inference engine parser.
;;(=>
;; (entails ?FORMULA1 ?FORMULA2)
;; (=> ?FORMULA1 ?FORMULA2))
(instance AssignmentFn Function)
(instance AssignmentFn VariableArityRelation)
(domain AssignmentFn 1 Function)
(domain AssignmentFn 2 Entity)
(range AssignmentFn Entity)
(documentation AssignmentFn EnglishLanguage "If F is a &%Function with a value for the
objects denoted by N1,..., NK, then (&%AssignmentFn F N1 ... NK) is the
value of applying F to the objects denoted by N1,..., NK. Otherwise,
the value is undefined.")
(instance PowerSetFn UnaryFunction)
(instance PowerSetFn TotalValuedRelation)
(domain PowerSetFn 1 SetOrClass)
(rangeSubclass PowerSetFn SetOrClass)
(documentation PowerSetFn EnglishLanguage "(&%PowerSetFn ?CLASS) maps the &%SetOrClass
?CLASS to the &%SetOrClass of all &%subclasses of ?CLASS.")
;; END FILE
;; BEGIN FILE
;;;;;;;;;;;;;;;;;;;;;;;
;; BASE ONTOLOGY ;;
;;;;;;;;;;;;;;;;;;;;;;;
;; INCLUDES 'STRUCTURAL ONTOLOGY'
;; The following hierarchy incorporates content from Sowa, Russell & Norvig,
;; and the top-level ontology from ITBM-CNR.
(partition Entity Physical Abstract)
(documentation Entity EnglishLanguage "The universal class of individuals. This is the root
node of the ontology.")
;; Informally, it is true that "Everything is Entity";
;; We comment out this axiom to avoid logical paradoxes.
;;(forall (?THING)
;; (instance ?THING Entity))
(exists (?THING)
(instance ?THING Entity))
(<=>
(instance ?CLASS Class)
(subclass ?CLASS Entity))
(subclass Physical Entity)
(partition Physical Object Process)
(documentation Physical EnglishLanguage "An entity that has a location in space-time.
Note that locations are themselves understood to have a location in
space-time.")
(=>
(instance ?PHYS Physical)
(exists (?LOC ?TIME)
(and
(located ?PHYS ?LOC)
(time ?PHYS ?TIME))))
(subclass Object Physical)
(documentation Object EnglishLanguage "Corresponds roughly to the class of ordinary
objects. Examples include normal physical objects, geographical regions,
and locations of &%Processes, the complement of &%Objects in the &%Physical
class. In a 4D ontology, an &%Object is something whose spatiotemporal
extent is thought of as dividing into spatial parts roughly parallel to the
time-axis.")
(subclass SelfConnectedObject Object)
(documentation SelfConnectedObject EnglishLanguage "A &%SelfConnectedObject is any
&%Object that does not consist of two or more disconnected parts.")
(subclass OrganicThing SelfConnectedObject)
(documentation OrganicThing EnglishLanguage "A &%SelfConnectedObject that is
produced by a non-intentional process from an &%Organism. Note that this
refers only to the primary cause. That is, a &%PlantAgriculturalProduct
is firstly produced by a &%Plant, and only secondarily by a &%Human that is
tending the plant.")
(instance FrontFn SpatialRelation)
(instance FrontFn PartialValuedRelation)
(instance FrontFn UnaryFunction)
(domain FrontFn 1 SelfConnectedObject)
(range FrontFn SelfConnectedObject)
(documentation FrontFn EnglishLanguage "A &%Function that maps an &%Object to the side
that generally receives the most attention or that typically faces the
direction in which the &%Object moves. Note that this is a partial
function, since some &%Objects do not have sides, e.g. apples and
spheres. Note too that the &%range of this &%Function is indefinite in
much the way that &%ImmediateFutureFn and &%ImmediatePastFn are indefinite.
Although this indefiniteness is undesirable from a theoretical standpoint,
it does not have significant practical implications, since there is
widespread intersubjective agreement about the most common cases.")
(=>
(instance ?OBJ SelfConnectedObject)
(side (FrontFn ?OBJ) ?OBJ))
(instance BackFn SpatialRelation)
(instance BackFn PartialValuedRelation)
(instance BackFn UnaryFunction)
(domain BackFn 1 SelfConnectedObject)
(range BackFn SelfConnectedObject)
(documentation BackFn EnglishLanguage "A &%Function that maps an &%Object to the side
that is opposite the &%FrontFn of the &%Object. Note that this is a
partial function, since some &%Objects do not have sides, e.g. apples
and spheres. Note too that the &%range of this &%Function is indefinite in
much the way that &%ImmediateFutureFn and &%ImmediatePastFn are indefinite.
Although this indefiniteness is undesirable from a theoretical standpoint,
it does not have significant practical implications, since there is
widespread intersubjective agreement about the most common cases.")
(=>
(instance ?OBJ SelfConnectedObject)
(side (BackFn ?OBJ) ?OBJ))
(instance part SpatialRelation)
(instance part PartialOrderingRelation)
(instance part BinaryPredicate)
(domain part 1 Object)
(domain part 2 Object)
(documentation part EnglishLanguage "The basic mereological relation. All other
mereological relations are defined in terms of this one.
(&%part ?PART ?WHOLE) simply means that the &%Object ?PART is part
of the &%Object ?WHOLE. Note that, since &%part is a
&%ReflexiveRelation, every &%Object is a part of itself.")
(instance properPart AsymmetricRelation)
(instance properPart TransitiveRelation)
(subrelation properPart part)
(documentation properPart EnglishLanguage "(&%properPart ?OBJ1 ?OBJ2) means that
?OBJ1 is a part of ?OBJ2 other than ?OBJ2 itself. This is a
&%TransitiveRelation and &%AsymmetricRelation (hence an
&%IrreflexiveRelation).")
(<=>
(properPart ?OBJ1 ?OBJ2)
(and
(part ?OBJ1 ?OBJ2)
(not
(part ?OBJ2 ?OBJ1))))
(subrelation piece part)
(instance piece BinaryPredicate)
(domain piece 1 Substance)
(domain piece 2 Substance)
(documentation piece EnglishLanguage "A specialized common sense notion of part for
arbitrary parts of &%Substances. Quasi-synonyms are: chunk, hunk, bit,
etc. Compare &%component, another subrelation of &%part.")
(=>
(piece ?SUBSTANCE1 ?SUBSTANCE2)
(forall (?CLASS)
(=>
(instance ?SUBSTANCE1 ?CLASS)
(instance ?SUBSTANCE2 ?CLASS))))
(subrelation component part)
(instance component BinaryPredicate)
(domain component 1 CorpuscularObject)
(domain component 2 CorpuscularObject)
(documentation component EnglishLanguage "A specialized common sense notion of part
for heterogeneous parts of complexes. (&%component ?COMPONENT ?WHOLE)
means that ?COMPONENT is a component of ?WHOLE. Examples of component
include the doors and walls of a house, the states or provinces of a
country, or the limbs and organs of an animal. Compare &%piece, which
is also a subrelation of &%part.")
(instance material BinaryPredicate)
(domainSubclass material 1 Substance)
(domain material 2 CorpuscularObject)
(documentation material EnglishLanguage "(&%material ?SUBSTANCE ?OBJECT) means that
?OBJECT is structurally made up in part of ?SUBSTANCE. This relation
encompasses the concepts of 'composed of', 'made of', and 'formed of'.
For example, plastic is a &%material of my computer monitor. Compare
&%part and its subrelations, viz &%component and &%piece.")
(=>
(contains ?SMALL ?BIG)
(partlyLocated ?SMALL ?BIG))
(instance contains SpatialRelation)
(instance contains AsymmetricRelation)
(instance contains PartialValuedRelation)
(instance contains BinaryPredicate)
(disjointRelation contains part)
(domain contains 1 SelfConnectedObject)
(domain contains 2 Object)
(documentation contains EnglishLanguage "The relation of spatial containment for two
separable objects. When the two objects are not separable (e.g. an
automobile and one of its seats), the relation of &%part should be used.
(&%contains ?OBJ1 ?OBJ2) means that the &%SelfConnectedObject ?OBJ1 has
a space (i.e. a &%Hole) which is at least partially filled by ?OBJ2.")
(<=>
(contains ?OBJ1 ?OBJ2)
(exists (?HOLE)
(and
(hole ?HOLE ?OBJ1)
(properlyFills ?OBJ2 ?HOLE))))
(subclass Substance SelfConnectedObject)
(partition Substance PureSubstance Mixture)
(partition Substance SyntheticSubstance NaturalSubstance)
(documentation Substance EnglishLanguage "An &%Object in which every part is similar to
every other in every relevant respect. More precisely, something is a
&%Substance when it has only arbitrary pieces as parts - any parts have
properties which are similar to those of the whole. Note that a &%Substance
may nonetheless have physical properties that vary. For example, the
temperature, chemical constitution, density, etc. may change from one part
to another. An example would be a body of water.")
(=>
(and
(subclass ?OBJECTTYPE Substance)
(instance ?OBJECT ?OBJECTTYPE)
(piece ?PART ?OBJECT))
(instance ?PART ?OBJECTTYPE))
(=>
(and
(instance ?OBJ Substance)
(attribute ?OBJ ?ATTR)
(piece ?PART ?OBJ))
(attribute ?PART ?ATTR))
(subclass SyntheticSubstance Substance)
(documentation SyntheticSubstance EnglishLanguage "Any &%Substance that is the result of
an &%IntentionalProcess, i.e. any substance that is created by &%Humans.")
(<=>
(instance ?SUBSTANCE SyntheticSubstance)
(exists (?PROCESS)
(and
(instance ?PROCESS IntentionalProcess)
(result ?PROCESS ?SUBSTANCE)
(instance ?SUBSTANCE Substance))))