-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathsumo++.kif
19686 lines (16105 loc) · 647 KB
/
sumo++.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
;; Access to and use of this file is governed by the GNU General
;; Public License <http://www.gnu.org/copyleft/gpl.html>.
;; This file contains modified versions of SUMO and three domain
;; ontologies. The effective date of modification is 2003-01-22.
;; Please refer to the accompanying documentation (sumo2loom_doc
;; rev. 2003-01-22 or similar) for a detailed explanation of the
;; modifications.
;; This file is distributed in the hope that it will be useful, but
;; WITHOUT ANY WARRANTY; without even the implied warranty of
;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. NIST does not
;; assume legal liability or responsibility for anything done with
;; this file.
;; Please refer to sumo2loom_doc for details of the copyright and
;; licensing terms.
;; ================================================
;; SUMO (Suggested Upper Merged Ontology)
;; ================================================
;; This is the source file for the SUMO (Suggested Upper Merged Ontology),
;; an ontology that was developed within the SUO Working Group by merging
;; the SUO "candidate content" sources and refining and extending this content on
;; the basis of various knowledge engineering projects and input from the SUO
;; Working Group.
;; The SUMO incorporates elements of John Sowa's upper ontology (as described at
;; http://www.bestweb.net/~sowa/ontology/toplevel.htm and in Chapter 2 of his
;; book _Knowledge Representation_, Brooks/Cole, 2000), Russell and Norvig's
;; ontology, PSL (Process Specification Language), Casati and Varzi's theory of
;; holes, Allen's temporal axioms, the relatively noncontroversial elements of
;; Smith's and Guarino's respective mereotopologies, the KIF formalization of the
;; CPR (Core Plan Representation), the ontologies available on the Ontolingua
;; server maintained by Stanford University's Knowledge Systems Laboratory, the
;; ontologies developed by ITBM-CNR, some of the spatial relations from an
;; unpublished paper by Iris Tommelein and Anil Gupta entitled "Conceptual
;; Structures for Spatial Reasoning", and a "Structural Ontology" proposed by
;; David Whitten and substantially revised and extended by Chris Menzel.
;; Note that some of the subclasses of 'Process' in the SUMO were originally
;; inspired by some of the verb classes from the second part of Beth Levin's book
;; "English Verb Classes and Alternations: A Preliminary Investigation."
;; 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://suo.ieee.org/suo-kif.html. It
;; should be noted that some of the axioms in the SUMO make use of row variables
;; (indicated with a "@" prefix). Such variables are not currently part of the SUO-
;; KIF specification, but they simplify matters significantly in some cases. Details
;; about row variables can be found in the following paper:
;; http://reliant.teknowledge.com/IJCAI01/HayesMenzel-SKIF-IJCAI2001.pdf.
;; 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. The dependencies between the
;; various subontologies can also be graphed informally as follows:
;;
;; STRUCTURAL ONTOLOGY
;; +
;; |
;; |
;; +
;; BASE ONTOLOGY
;; / | | \
;; / | | \
;; / | | \
;; / | | \
;; / | | \
;; + + + +
;; SET/CLASS THEORY NUMERIC TEMPORAL MEREOTOPOLOGY
;; / | | |
;; / | | |
;; / | | |
;; + + + +
;; GRAPH MEASURE PROCESSES +--+ OBJECTS
;; + +
;; \ /
;; \ /
;; \ /
;; + +
;; QUALITIES
;;
;;
;; Note that the "+" sign at the end of an arc indicates the direction of
;; dependency - the node near the sign includes the subontology at the other
;; end of the arc. Note too that in some cases the dependency is
;; bidirectional. Separating ontologies in cases like these is useful when
;; their respective topics can be cleanly differentiated.
;; 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 SetOrClass)
(documentation instance "An object is an &%instance of a &%SetOrClass if
it is included in that &%SetOrClass. 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 "An object is an &%immediateInstance of
a &%SetOrClass if it is an instance of the &%SetOrClass and there does not exist a
subclass of &%SetOrClass such that it is an instance of the subclass.")
(=>
(immediateInstance ?ENTITY ?CLASS)
(not (exists (?SUBCLASS)
(and
(subclass ?SUBCLASS ?CLASS)
(instance ?ENTITY ?SUBCLASS)))))
(instance inverse BinaryPredicate)
(domain inverse 1 BinaryRelation)
(domain inverse 2 BinaryRelation)
(documentation inverse "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.")
(=>
(inverse ?REL1 ?REL2)
(forall (?INST1 ?INST2)
(<=>
(holds ?REL1 ?INST1 ?INST2)
(holds ?REL2 ?INST2 ?INST1))))
(instance subclass BinaryPredicate)
(instance subclass PartialOrderingRelation)
(domain subclass 1 SetOrClass)
(domain subclass 2 SetOrClass)
(documentation subclass "(&%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 ?SUBCLASS ?CLASS)
(forall (?INST)
(=>
(instance ?INST ?SUBCLASS)
(instance ?INST ?CLASS))))
(subrelation immediateSubclass subclass)
(instance immediateSubclass AsymmetricRelation)
(instance immediateSubclass IntransitiveRelation)
(documentation immediateSubclass "A &%SetOrClass ?CLASS1 is an &%immediateSubclass
of another &%SetOrClass ?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 "A &%Relation R is a &%subrelation
&%Relation R' if R is a &%subclass R'. This implies that every
tuple of R is also a tuple of R'. Again, if R holds for some arguments
arg_1, arg_2, ... arg_n, then R' holds for the same arguments. Thus, a
&%Relation and its subrelation must have the same valence. In CycL,
&%subrelation is called #$genlPreds.")
(=>
(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)
(holds ?REL1 @ROW))
(holds ?REL2 @ROW))
(=>
(and
(subrelation ?PRED1 ?PRED2)
(instance ?PRED2 ?CLASS)
(instance ?CLASS InheritableRelation))
(instance ?PRED1 ?CLASS))
(instance domain TernaryPredicate)
(domain domain 1 Relation)
(domain domain 2 PositiveInteger)
(domain domain 3 SetOrClass)
(documentation domain "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
&%SetOrClass already defined in the ontology, one can specify a &%SetOrClass
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 SetOrClass)
(documentation domainSubclass "&%Predicate 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 ?REL1 ?NUMBER ?CLASS2))
(domainSubclass ?REL2 ?NUMBER ?CLASS2))
(=>
(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 "(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 ?THING1 ?THING2)
(forall (?CLASS)
(<=>
(instance ?THING1 ?CLASS)
(instance ?THING2 ?CLASS))))
(instance range BinaryPredicate)
(instance range AsymmetricRelation)
(domain range 1 Function)
(domain range 2 SetOrClass)
(documentation range "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 ?REL1 ?CLASS1))
(range ?REL2 ?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 SetOrClass)
(documentation rangeSubclass "(&%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 ?REL1 ?CLASS1))
(rangeSubclass ?REL2 ?CLASS1))
(=>
(and
(rangeSubclass ?REL ?CLASS1)
(rangeSubclass ?REL ?CLASS2))
(or
(subclass ?CLASS1 ?CLASS2)
(subclass ?CLASS2 ?CLASS1)))
(instance DomainFn UnaryFunction)
(domain DomainFn 1 BinaryRelation)
(range DomainFn SetOrClass)
(documentation DomainFn "The domain of a &%BinaryRelation ?REL is
the &%SetOrClass of all things that bear ?REL to something.")
(<=>
(instance ?INST1 (DomainFn ?REL))
(exists (?INST2)
(holds ?REL ?INST1 ?INST2)))
(=>
(instance ?REL BinaryRelation)
(domain ?REL 2 (DomainFn ?REL)))
(instance RangeFn UnaryFunction)
(domain RangeFn 1 BinaryRelation)
(range RangeFn SetOrClass)
(documentation RangeFn "The range of a &%BinaryRelation ?REL is the
&%SetOrClass of all things such that something bears ?REL to them.")
(<=>
(instance ?INST1 (RangeFn ?REL))
(exists (?INST2)
(holds ?REL ?INST2 ?INST1)))
(=>
(instance ?REL UnaryFunction)
(range ?REL (RangeFn ?REL)))
(=>
(instance ?REL BinaryPredicate)
(domain ?REL 2 (RangeFn ?REL)))
(instance valence BinaryPredicate)
(instance valence AsymmetricRelation)
(instance valence SingleValuedRelation)
(domain valence 1 Relation)
(domain valence 2 PositiveInteger)
(documentation valence "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. For example, &%holds is a
&%VariableArityRelation.")
(instance documentation BinaryPredicate)
(instance documentation AsymmetricRelation)
(domain documentation 1 Entity)
(domain documentation 2 SymbolicString)
(documentation documentation "A relation between objects in the domain
of discourse and strings of natural language text. 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 disjoint BinaryPredicate)
(instance disjoint SymmetricRelation)
(instance disjoint IrreflexiveRelation)
(domain disjoint 1 SetOrClass)
(domain disjoint 2 SetOrClass)
(documentation disjoint "&%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 Predicate)
(instance disjointRelation VariableArityRelation)
(relatedInternalConcept disjointRelation disjoint)
(documentation disjointRelation "This predicate relates any number of &%Relations.
(&%disjointRelation @ROW) means that any two relations in @ROW have no tuples in
common. As a consequence, the intersection of all of the relations in @ROW is the
null set.")
(=>
(and
(disjointRelation @ROW)
(inList ?REL (ListFn @ROW)))
(instance ?REL Relation))
(=>
(and
(disjointRelation @ROW)
(inList ?REL1 (ListFn @ROW))
(inList ?REL2 (ListFn @ROW))
(valence ?REL1 ?NUMBER))
(valence ?REL2 ?NUMBER))
(=>
(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
(disjointRelation @ROW1)
(inList ?REL1 (ListFn @ROW1))
(inList ?REL2 (ListFn @ROW1))
(holds ?REL1 @ROW2))
(not (holds ?REL2 @ROW2)))
(instance contraryAttribute Predicate)
(instance contraryAttribute VariableArityRelation)
(documentation contraryAttribute "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)))
(=>
(contraryAttribute @ROW)
(forall (?ATTR1 ?ATTR2)
(=>
(and
(inList ?ATTR1 (ListFn @ROW))
(inList ?ATTR2 (ListFn @ROW))
(not (equal ?ATTR1 ?ATTR2)))
(=>
(property ?OBJ ?ATTR1)
(not (property ?OBJ ?ATTR2))))))
(instance exhaustiveAttribute Predicate)
(instance exhaustiveAttribute VariableArityRelation)
(domainSubclass exhaustiveAttribute 1 Attribute)
(documentation exhaustiveAttribute "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 &%Liquid &%Gas) means that there are only three instances of the class
&%PhysicalState, viz. &%Solid, &%Liquid, and &%Gas.")
(=>
(exhaustiveAttribute ?CLASS @ROW)
(=>
(inList ?ATTR (ListFn @ROW))
(instance ?ATTR Attribute)))
(=>
(exhaustiveAttribute ?CLASS @ROW)
(forall (?OBJ)
(=>
(instance ?ATTR1 ?CLASS)
(exists (?ATTR2)
(and
(inList ?ATTR2 (ListFn @ROW))
(equal ?ATTR1 ?ATTR2))))))
(instance exhaustiveDecomposition Predicate)
(instance exhaustiveDecomposition VariableArityRelation)
(domain exhaustiveDecomposition 1 Class)
(relatedInternalConcept exhaustiveDecomposition partition)
(documentation exhaustiveDecomposition "An &%exhaustiveDecomposition of a
&%Class C is a set of subclasses of C such that every subclass of C either
is an element of the set or is a subclass of an element of 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)
(relatedInternalConcept disjointDecomposition exhaustiveDecomposition)
(relatedInternalConcept disjointDecomposition disjoint)
(documentation disjointDecomposition "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)
(documentation partition "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 "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 "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)
(disjointRelation synonymousExternalConcept subsumedExternalConcept subsumingExternalConcept)
(documentation synonymousExternalConcept "(&%synonymousExternalConcept
?STRING ?THING ?LANGUAGE) means that the SUMO concept ?THING has the
same meaning as ?STRING in ?LANGUAGE.")
(subrelation subsumingExternalConcept relatedExternalConcept)
(documentation subsumingExternalConcept "(&%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)
(documentation subsumedExternalConcept "(&%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 subAttribute BinaryPredicate)
(instance subAttribute PartialOrderingRelation)
(domain subAttribute 1 Attribute)
(domain subAttribute 2 Attribute)
(disjointRelation subAttribute successorAttribute)
(documentation subAttribute "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 "(&%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)
(domain successorAttributeClosure 1 Attribute)
(domain successorAttributeClosure 2 Attribute)
(relatedInternalConcept successorAttributeClosure successorAttribute)
(documentation successorAttributeClosure "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 and LogicalOperator)
(domain and 1 Formula)
(domain and 2 Formula)
(documentation and "The truth-functional connective of conjunction.")
(instance or LogicalOperator)
(domain or 1 Formula)
(domain or 2 Formula)
(documentation or "The truth-functional connective of disjunction.")
(instance => LogicalOperator)
(domain => 1 Formula)
(domain => 2 Formula)
(documentation => "The truth-functional connective of implication.")
(instance <=> LogicalOperator)
(domain <=> 1 Formula)
(domain <=> 2 Formula)
(documentation <=> "The truth-functional connective of bi-implication.")
(instance not LogicalOperator)
(domain not 1 Formula)
(documentation not "The truth-functional connective of negation.")
(instance forall LogicalOperator)
(domain forall 1 List)
(domain forall 2 Formula)
(documentation forall "The universal quantifier of predicate logic.")
(instance exists LogicalOperator)
(domain exists 1 List)
(domain exists 2 Formula)
(documentation exists "The existential quantifier of predicate logic.")
(instance entails LogicalOperator)
(domain entails 1 Formula)
(domain entails 2 Formula)
(documentation entails "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.")
(=>
(entails ?FORMULA1 ?FORMULA2)
(=> ?FORMULA1 ?FORMULA2))
(instance AssignmentFn Function)
(instance AssignmentFn VariableArityRelation)
(domain AssignmentFn 1 Function)
(range AssignmentFn Entity)
(documentation AssignmentFn "If F is a function with a value for the
objects denoted by N1,..., NK, then the term (AssignmentFn F N1 ... NK)
denotes the value of applying F to the objects denoted by N1,..., NK.
Otherwise, the value is undefined.")
(instance holds Predicate)
(instance holds VariableArityRelation)
(domain holds 1 Relation)
(documentation holds "(holds P N1 ... NK) is true just in case
the tuple of objects denoted by N1,..., NK is an element of
the &%Relation P.")
(<=>
(and
(holds ?REL @ROW ?INST)
(instance ?REL Function))
(equal (AssignmentFn ?REL @ROW) ?INST))
(=>
(instance ?REL Predicate)
(<=>
(holds ?REL @ROW)
(?REL @ROW)))
(instance PowerSetFn UnaryFunction)
(domain PowerSetFn 1 SetOrClass)
(rangeSubclass PowerSetFn SetOrClass)
(documentation PowerSetFn "(&%PowerSetFn ?CLASS) maps the &%SetOrClass
?CLASS to the &%SetOrClass of all &%subclasses of ?CLASS.")
(<=>
(instance ?SUBCLASS (PowerSetFn ?CLASS))
(subclass ?SUBCLASS ?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.
(documentation Entity "The universal class of individuals. This is the root
node of the ontology.")
(instance ?THING Entity)
(exists (?THING) (instance ?THING Entity))
(=>
(instance ?CLASS Class)
(subclass ?CLASS Entity))
(subclass Physical Entity)
(partition Physical Object Process)
(documentation Physical "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 "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 "A &%SelfConnectedObject is any
&%Object that does not consist of two or more disconnected parts.")
(instance FrontFn SpatialRelation)
(instance FrontFn UnaryFunction)
(instance FrontFn AsymmetricRelation)
(instance FrontFn IrreflexiveRelation)
(domain FrontFn 1 SelfConnectedObject)
(range FrontFn SelfConnectedObject)
(documentation FrontFn "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)
(part (FrontFn ?OBJ) ?OBJ))
(instance BackFn SpatialRelation)
(instance BackFn UnaryFunction)
(instance BackFn AsymmetricRelation)
(instance BackFn IrreflexiveRelation)
(domain BackFn 1 SelfConnectedObject)
(range BackFn SelfConnectedObject)
(documentation BackFn "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)
(part (BackFn ?OBJ) ?OBJ))
(subrelation part located)
(instance part SpatialRelation)
(instance part PartialOrderingRelation)
(domain part 1 Object)
(domain part 2 Object)
(documentation part "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 "(&%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)
(domain piece 1 Substance)
(domain piece 2 Substance)
(documentation piece "A specialized common sense notion of part for
arbitrary parts of &%Substances. Quasi-synonyms are: chunk, hunk, bit,
etc. Compare &%component, the other subrelation of &%part.")
(=>
(piece ?SUBSTANCE1 ?SUBSTANCE2)
(forall (?CLASS)
(=>
(instance ?SUBSTANCE1 ?CLASS)
(instance ?SUBSTANCE2 ?CLASS))))
(subrelation component part)
(domain component 1 CorpuscularObject)
(domain component 2 CorpuscularObject)
(documentation component "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 "(&%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.")
(subclass Substance SelfConnectedObject)
(documentation Substance "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)
(part ?PART ?OBJECT))
(instance ?PART ?OBJECTTYPE))
(=>
(and
(instance ?OBJ Substance)
(attribute ?OBJ ?ATTR)
(part ?PART ?OBJ))
(attribute ?PART ?ATTR))
(subclass PureSubstance Substance)
(partition PureSubstance CompoundSubstance ElementalSubstance)
(documentation PureSubstance "The &%Class of &%Substances with constant
composition. A &%PureSubstance can be either an element (&%ElementalSubstance)
or a compound of elements (&%CompoundSubstance). Examples: Table salt
(sodium chloride, NaCl), sugar (sucrose, C_{12}H_{22}O_{11}), water (H_2O),
iron (Fe), copper (Cu), and oxygen (O_2).")
(subclass ElementalSubstance PureSubstance)
(documentation ElementalSubstance "The &%Class of &%PureSubstances that
cannot be separated into two or more &%Substances by ordinary chemical
(or physical) means. This excludes nuclear reactions. &%ElementalSubstances
are composed of only one kind of atom. Examples: Iron (Fe), copper (Cu),
and oxygen (O_2). &%ElementalSubstances are the simplest
&%PureSubstances.")
(subclass Metal ElementalSubstance)
(documentation Metal "A &%Metal is an &%ElementalSubstance that conducts heat
and electricity, is shiny and reflects many colors of light, and can be hammered
into sheets or drawn into wire. About 80% of the known chemical elements
(&%ElementalSubstances) are metals.")
(subclass Atom ElementalSubstance)
(documentation Atom "An extremely small unit of matter that retains its
identity in Chemical reactions. It consists of an &%AtomicNucleus and
&%Electrons surrounding the &%AtomicNucleus.")
(=>
(instance ?ATOM Atom)
(exists (?PROTON ?ELECTRON)
(and
(component ?PROTON ?ATOM)
(component ?ELECTRON ?ATOM)
(instance ?PROTON Proton)
(instance ?ELECTRON Electron))))
(=>
(instance ?ATOM Atom)
(forall (?NUCLEUS1 ?NUCLEUS2)
(=>
(and
(component ?NUCLEUS1 ?ATOM)
(component ?NUCLEUS2 ?ATOM)
(instance ?NUCLEUS1 AtomicNucleus)
(instance ?NUCLEUS2 AtomicNucleus))
(equal ?NUCLEUS1 ?NUCLEUS2))))
(subclass SubatomicParticle ElementalSubstance)
(documentation SubatomicParticle "The class of &%ElementalSubstances that
are smaller than &%Atoms and compose &%Atoms.")
(=>
(instance ?PARTICLE SubatomicParticle)
(exists (?ATOM)
(and
(instance ?ATOM Atom)
(part ?PARTICLE ?ATOM))))
(subclass AtomicNucleus SubatomicParticle)
(documentation AtomicNucleus "The core of the &%Atom. It is composed of
&%Protons and &%Neutrons.")
(=>
(instance ?NUCLEUS AtomicNucleus)
(exists (?NEUTRON ?PROTON)
(and
(component ?NEUTRON ?NUCLEUS)
(component ?PROTON ?NUCLEUS)
(instance ?NEUTRON Neutron)
(instance ?PROTON Proton))))
(subclass Electron SubatomicParticle)
(documentation Electron "&%SubatomicParticles that surround the
&%AtomicNucleus. They have a negative charge.")
(subclass Proton SubatomicParticle)
(documentation Proton "Components of the &%AtomicNucleus. They have a
positive charge.")
(subclass Neutron SubatomicParticle)
(documentation Neutron "Components of the &%AtomicNucleus. They have no
charge.")
(subclass CompoundSubstance PureSubstance)
(documentation CompoundSubstance "The &%Class of &%Substances that contain
two or more elements (&%ElementalSubstances), in definite proportion by weight.
The composition of a pure compound will be invariant, regardless of the method
of preparation. Compounds are composed of more than one kind of atom (element).
The term molecule is often used for the smallest unit of a compound that still
retains all of the properties of the compound. Examples: Table salt (sodium
chloride, NaCl), sugar (sucrose, C_{12}H_{22}O_{11}), and water (H_2O). ")
(subclass Mixture Substance)
(documentation Mixture "A &%Mixture is two or more &%PureSubstances,
combined in varying proportions - each retaining its own specific properties.
The components of a &%Mixture can be separated by physical means, i.e. without
the making and breaking of chemical bonds. Examples: Air, table salt thoroughly
dissolved in water, milk, wood, and concrete. ")