This repository has been archived by the owner on Jan 17, 2018. It is now read-only.
forked from ontologyportal/sumo
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Merge.kif
executable file
·18248 lines (15857 loc) · 755 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 SetOrClass)
(documentation instance EnglishLanguage "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.")
(documentation instance ChineseLanguage "如果一个物体属于一个&%SetOrClass, 这物体就那个 &%SetOrClass的一个&%instance。 一个个体可以是许多类别的一个&%instance, 其中有一些可以是其他类别 的子类别,所以对于&%instance并没有假设任何具体或独特的含义。")
(subrelation immediateInstance instance)
(instance immediateInstance AsymmetricRelation)
(instance immediateInstance IntransitiveRelation)
(instance immediateInstance TotalValuedRelation)
(documentation immediateInstance EnglishLanguage "An object is an &%immediateInstance of
a &%SetOrClass if it is an &%instance of the &%SetOrClass and it is not an
&%instance of a proper subclass of &%SetOrClass.")
(documentation immediateInstance ChineseLanguage "如果一个物体是一个&%SetOrClass的
&%instance,而且它并不是该&%SetOrClass真正的子类别的&%instance,那这个物体就是该&%SetOrClass的
&%immediateInstance。")
(=>
(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.")
(documentation inverse ChineseLanguage "&%BinaryRelation的相反是一种&%Relation,而属于它
原本&%Relation所有元组的值都逆转。 换句话说,当一种二元关系和另一种二元关系的参数交换的结果是相等的
话,那这&%BinaryRelation就是另一种的相反。")
; 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 SetOrClass)
(domain subclass 2 SetOrClass)
(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.")
(documentation subclass ChineseLanguage "(&%subclass ?CLASS1 ?CLASS2) 的意思是 ?CLASS1 是
?CLASS2 的&%subclass,也就是说, ?CLASS1 的每一个&%instance同时也是 ?CLASS2 的一个&%instance。
一个&%Class可以具有多个超类别和子类别。")
(=>
(subclass ?X ?Y)
(and
(instance ?X SetOrClass)
(instance ?Y SetOrClass)))
(=>
(and
(subclass ?X ?Y)
(instance ?Z ?X))
(instance ?Z ?Y))
(subrelation immediateSubclass subclass)
(instance immediateSubclass AsymmetricRelation)
(instance immediateSubclass IntransitiveRelation)
(documentation immediateSubclass EnglishLanguage "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.")
(documentation immediateSubclass ChineseLanguage "一个&%SetOrClass的 ?CLASS1 是另一个
&%SetOrClass ?CLASS2 的&%immediateSubclass, 为免 ?CLASS1 成为 ?CLASS2 的子类别,而 ?CLASS2
再没有子类别,这样 ?CLASS1 也是 ?CLASS2 的子类别。")
(=>
(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.")
(documentation subrelation ChineseLanguage "(&%subrelation ?REL1 ?REL2)的意思是
?REL1的每个元组也是?REL2的元组。 也就是说,如果 ?REL1的一些参数 arg_1,arg_2,... arg_n
的&%Relation成立的话,那么?REL2的相同参数的 &%Relation也同样成立。 因此, 一个&%Relation和它
的&%subrelation必须拥有相同的&%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 SetOrClass)
(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
&%SetOrClass already defined in the ontology, one can specify a &%SetOrClass
compositionally with the functions &%UnionFn, &%IntersectionFn, etc.")
(documentation domain ChineseLanguage "为声明某种特定关系参数的类型, 提供一个便利计算机和应用启发
式运算的机制。公式(&%domain?REL?INT?CLASS)的意思是在?REL关系中,每个元组的第?INT个元素,必须是
?CLASS种的一个实例。 指定参数类型对维护知识本体甚有裨益。 表示知识的系统可以使用这些规范来把术语分类, 并
检查系统的完整性约束有否受到破坏。如果出现某个%Relation参数类型的限制,还没有在知识本体内现有
&%SetOrClass定义所描述时,可以使用&%UnionFn和&%IntersectionFn等这些功能,来逐一指定该
&%SetOrClass的限制。
")
(=>
(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 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.")
(documentation domainSubclass ChineseLanguage "这个 &%Predicate 是用来指定 &%Predicates 参数
类型的限制。 公式(&%domainSubclass ?REL ?INT ?CLASS) 的意思是在?REL关系中,每个元组的第?INT个元素,
必须是?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.")
(documentation equal ChineseLanguage "假如 ?ENTITY1 等于 ?ENTITY2的话,那么
(equal ?ENTITY1 ?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 SetOrClass)
(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.")
(documentation range ChineseLanguage "它为函数提供一个范围。就是说,(&%range ?FUNCTION ?CLASS)
的意思是,所有由 ?FUNCTION 所指定的值,都是这个 ?CLASS 的 &%instance。")
(=>
(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 SetOrClass)
(documentation rangeSubclass EnglishLanguage "(&%rangeSubclass ?FUNCTION ?CLASS) means
that all of the values assigned by ?FUNCTION are &%subclasses of ?CLASS.")
(documentation rangeSubclass ChineseLanguage "(&%rangeSubclass ?FUNCTION ?CLASS) 的意思是
所有由 ?FUNCTION 所指定的值,都是这个 ?CLASS 的 &%subclass。")
(=>
(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.")
(documentation valence ChineseLanguage "指定一个关系可接纳参数的数目。 如果一个关系没有设定参数
数目,那么它就没有配价,它也就是 &%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.")
(documentation documentation ChineseLanguage "在话语领域和自然语言的字符串,以某种
&%HumanLanguage 来陈述的物件之间一种关系。 &%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.")
(documentation format ChineseLanguage "这是一种关系,用于指定如何以自然语言格式来介绍表达式。")
(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.")
(documentation termFormat ChineseLanguage "这是一种关系,用于指定如何以自然语言格式来介绍一个术语。")
(instance disjoint BinaryPredicate)
(instance disjoint SymmetricRelation)
(domain disjoint 1 SetOrClass)
(domain disjoint 2 SetOrClass)
(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.")
(documentation disjoint ChineseLanguage "如果&%Class 和 &%Class之间没有共同案例的话, 那么它们
就是 &%disjoint,也就是以防万一应用 &%IntersectionFn 的时候出现空的的结果。")
(=>
(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.")
(documentation disjointRelation ChineseLanguage "这个术语把两种 &%Relation 连接。
(&%disjointRelation ?REL1 ?REL2) 的意思是指这两种关系没有共同的元组。")
(=>
(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)
(not (equal ?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.")
(documentation contraryAttribute ChineseLanguage "&%contraryAttribute 是一组 &%Attribute
,而某一件事物不能同时拥有超过一种这个组里的 &%Attributes。 举例说:
(&%contraryAttribute &%Pliable &%Rigid) 指的是没有一件东西是既 &%Pliable 又 &%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.")
(documentation exhaustiveAttribute ChineseLanguage "这个术语把一个 &%Class 联系到一组
&%Attribute, 就是说这个组的单元已经是这个 &%Class 所有的实例。举例说: (&%exhaustiveAttribute
&%PhysicalState &%Solid &%Fluid &%Liquid &%Gas &%Plasma) 的意思是 &%PhysicalState 这个类别就
只有 &%Solid,&%Fluid, &%Liquid, &%Gas 和 &%Plasma 这五个实例了。")
(=>
(exhaustiveAttribute ?CLASS @ROW)
(=>
(inList ?ATTR (ListFn @ROW))
(instance ?ATTR Attribute)))
(=>
(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)))))))))
(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).")
(documentation exhaustiveDecomposition ChineseLanguage "C &%Class 的
&%exhaustiveDecomposition 是C的一组子类别, 而C的每一个实例就是这个组内其中一个子类别的一个实例。按:
这并不一定是意会着这个组的单元都不相交 (可参考 &%partition - 一个 &%partition 是一个已列举尽
不相交的掏空成分。 ")
(=>
(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.")
(documentation disjointDecomposition ChineseLanguage "C &%Class 的 &%disjointDecomposition
是C的一组相互 &%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.")
(documentation partition ChineseLanguage "C &%Class 的 &%partition 是一组包括C,而互不
&%disjoint 的类别 (一个子类别的分区)。C的每一个实例正正是这个分区子类别的一个实例。")
(<=>
(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.")
(documentation relatedInternalConcept ChineseLanguage "这个意思是两个变量在SUMO是相关的概念,就是
说它们之间的含义极为相似。可以用 &%relatedExternalConcept 术语,来要表示一个SUMO概念和另一个出处的概念
在含义上的关系。")
(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.")
(documentation relatedExternalConcept ChineseLanguage "这是用来表示一个概念联系的三重关系:概念的
外部知识来源、 SUMO概念和它外部知识来源的名字。")
(subrelation synonymousExternalConcept relatedExternalConcept)
(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.")
(documentation synonymousExternalConcept ChineseLanguage "(&%synonymousExternalConcept
?STRING ?THING ?LANGUAGE) 的意思是SUMO概念 ?THING 和概念 ?STRING 在语言 ?LANGUAGE 的含义是相同
的。")
(subrelation subsumingExternalConcept relatedExternalConcept)
(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.")
(documentation subsumingExternalConcept ChineseLanguage "(&%subsumingExternalConcept
?STRING ?THING ?LANGUAGE) 的意思是SUMO概念 ?THING 包含了概念 ?STRING 在语言 ?LANGUAGE 的含义,
也就是说概念 ?THING 的含义比 ?STRING 要广。")
(subrelation subsumedExternalConcept relatedExternalConcept)
(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.")
(documentation subsumedExternalConcept ChineseLanguage "(&%subsumedExternalConcept
?STRING ?THING ?LANGUAGE) 的意思是SUMO概念 ?THING 被纳入概念 ?STRING 在语言 ?LANGUAGE 的含义,
也就是说概念 ?THING 的含义比 ?STRING 要窄。")
(instance externalImage BinaryPredicate)
(documentation externalImage EnglishLanguage "A link between an Entity and a
URL that represents or exemplifies the term in some way.")
(documentation externalImage ChineseLanguage "联系一个实体和在某方面代表或举例证明这个概念的网址。")
(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.")
(documentation subAttribute ChineseLanguage "这意思是第二个参数的属性可以归因于所有第一个参数
所归因的属性。")
(=>
(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.")
(documentation successorAttribute ChineseLanguage "(&%successorAttribute ?ATTR1 ?ATTR2)
的意思是在它们共同有的尺度上 &%Attribute ?ATTR2 是紧接着 ?ATTR1。")
(=>
(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.")
(documentation successorAttributeClosure ChineseLanguage "&%successorAttribute 的
传递闭包;(&%successorAttributeClosure ?ATTR1 ?ATTR2) 的意思是 &%successorAttribute 有一连串
联系着 ?ATTR1 和 ?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")
(documentation greaterThanByQuality ChineseLanguage "(greaterThanByQuality
?ENTITY1 ?ENTITY2 ?ATT) 的意思是 ?ENTITY1 既定的 ?ATT 量比 ?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.")
(documentation entails ChineseLanguage "这是逻辑蕴涵的运算符。(&%entails ?FORMULA1 ?FORMULA2)
的意思是 ?FORMULA2 可以通过SUO-KIF的证明理论从 ?FORMULA1 得出来。")
;; 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.")
(documentation AssignmentFn ChineseLanguage "如果F是一个 &%Function,它所代表物体的值以
N1,...,NK表示, 那么 (&%AssignmentFn F N1 ... NK) 就是应用F到这些物体以N1,..., NK所代表的值。
在其他情况下,这个值是没有被下定义的。")
(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.")
(documentation PowerSetFn ChineseLanguage "(&%PowerSetFn ?CLASS) 把&%SetOrClass ?CLASS
的所有&%subclass,都纳入&%SetOrClass的?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.")
(documentation Physical ChineseLanguage "存在时空中某位置的个体。注:位置本身应理解为,存在于某个时空
的位置。")
(=>
(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.")
(documentation Object ChineseLanguage "这可粗略地对应为一般物体。例子包括
正常物理对象、地理区域和 &%Process 的位置,在 &%Physical 类别 &%Object 的补充。
在四维本体论上, &%Object 的时空范畴可大致划分为与时间轴平行的空间间隔。")
(subclass SelfConnectedObject Object)
(documentation SelfConnectedObject EnglishLanguage "A &%SelfConnectedObject is any
&%Object that does not consist of two or more disconnected parts.")
(documentation SelfConnectedObject ChineseLanguage " &%SelfConnectedObject
是任何并非由两个或以上不相连部分所组成的 &%Object。")
(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.")
(documentation OrganicThing ChineseLanguage "这是一个从 &%Organism 通过非刻意过程所产生的
&%SelfConnectedObject。注:这里指只是主要原因,就是说 &%PlantAgriculturalProduct 首先从 &%Plant
生长出来,次要才由 &%Human 产生,约就是耕种植物。")
(instance FrontFn SpatialRelation)
(instance FrontFn PartialValuedRelation)
(instance FrontFn UnaryFunction)
(instance FrontFn AsymmetricRelation)
(instance FrontFn IrreflexiveRelation)
(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.")
(documentation FrontFn ChineseLanguage "这是一个&%Function ,它能把 &%Object 转到一般能够得到
最大程度关注或者说通常是面对该 &%Object 移动的方向的那一面。注:这是一个部分函数, 因为有一些 &%Object
是没有侧面的,例如苹果和球体。 也要注意这个 &%Function 的 &%range 是无限的,就像 &%ImmediateFutureFn
和 &%ImmediatePastFn 一样也是无限的。从理论的观点来说,虽然这个无限性并不理想,但它没有太大的实际影响,
因为在共同意思间对于最常见的情况已经达成广泛的共识。")
(=>
(instance ?OBJ SelfConnectedObject)
(side (FrontFn ?OBJ) ?OBJ))
(instance BackFn SpatialRelation)
(instance BackFn PartialValuedRelation)
(instance BackFn UnaryFunction)
(instance BackFn AsymmetricRelation)
(instance BackFn IrreflexiveRelation)
(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.")
(documentation BackFn ChineseLanguage "这个 &%Function 把 &%Object 转到 与 这个 &%Object 的
&%FrontFn 相反的那面。注:这是一个部分函数, 因为有一些 &%Object 是没有侧面的,例如苹果和球体。 也要注意
这个 &%Function 的 &%range 是无限的,就像 &%ImmediateFutureFn 和 &%ImmediatePastFn
一样也是无限的。从理论的观点来说,虽然这个无限性并不理想,但它没有太大的实际影响,因为在共同意思间对于最常见
的情况已经达成广泛的共识。")
(=>
(instance ?OBJ SelfConnectedObject)
(side (BackFn ?OBJ) ?OBJ))
(instance part SpatialRelation)
(instance part PartialOrderingRelation)
(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.")
(documentation part ChineseLanguage "这是基本的逻辑分体关系。其他所有的逻辑分体关系都是根据它来下
定义的。 (&%part ?PART ?WHOLE) 的意思就是 &%Object ?PART 是 &%Object ?WHOLE 的一部分。 要注意
因为 &%part 是一个 &%ReflexiveRelation, 所以每个 &%Object 都是它自己本身的一部分。")
(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).")
(documentation properPart ChineseLanguage "(&%properPart ?OBJ1 ?OBJ2) 的意思是除了 ?OBJ2 本身
?OBJ1 是 ?OBJ2 的一部分。 这是一个 &%TransitiveRelation 和 &%AsymmetricRelation (因此也是一个
&%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 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.")
(documentation piece ChineseLanguage "这是对 &%Substance 某些部分的一个专业常识概念。类似的同意词
有:块、大块、小块等。可参考比较 &%part 的另外一个子关系 &%component 。")
(=>
(piece ?SUBSTANCE1 ?SUBSTANCE2)
(forall (?CLASS)
(=>
(instance ?SUBSTANCE1 ?CLASS)
(instance ?SUBSTANCE2 ?CLASS))))
(subrelation component part)
(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