Browsing Interface : Welcome guest : log in 		[  Home |  Graph |  LogLearn |  Editor |  ]  KB:  Language: 
  Formal Language: 


KB Term:  Term intersection
English Word: 

Sigma KEE - systemPart
systemPart

appearance as argument number 1
-------------------------


(instance systemPart BinaryPredicate) Merge.kif 6253-6253 system part is an instance of binary predicate
(domain systemPart 1 Physical) Merge.kif 6254-6254 The number 1 argument of system part is an instance of physical
(domain systemPart 2 PhysicalSystem) Merge.kif 6255-6255 The number 2 argument of system part is an instance of physical system
(documentation systemPart EnglishLanguage "(systemPart ?PART ?SYSTEM) means that the Physical thing ?PART is a SystemElement in the PhysicalSystem ?SYSTEM.") Merge.kif 6257-6259 The number 2 argument of system part is an instance of physical system

appearance as argument number 2
-------------------------


(format EnglishLanguage systemPart "%2 is %n a system part of %1") domainEnglishFormat.kif 2437-2437
(format ChineseTraditionalLanguage systemPart "%2 %n 是 %1 的 system 部分") domainEnglishFormat.kif 2438-2438
(format ChineseLanguage systemPart "%2 %n 是 %1 的 system 部分") domainEnglishFormat.kif 2439-2439
(termFormat EnglishLanguage systemPart "system part") domainEnglishFormat.kif 56666-56666
(termFormat ChineseTraditionalLanguage systemPart "系統部分") domainEnglishFormat.kif 56667-56667
(termFormat ChineseLanguage systemPart "系统部分") domainEnglishFormat.kif 56668-56668

antecedent
-------------------------


(=>
    (and
        (subSystem ?SUB ?SYSTEM)
        (systemPart ?PART ?SUB))
    (systemPart ?PART ?SYSTEM))		 Merge.kif 6261-6265 If X is a sub system of Y and Y is a system part of Z, then X is a system part of Z
(=>
    (and
        (instance ?TS TransitSystem)
        (instance ?T Transitway)
        (abstractCounterpart ?G ?TS)
        (systemPart ?T ?TS))
    (exists (?GA)
        (and
            (instance ?GA GraphArc)
            (abstractCounterpart ?GA ?T)
            (graphPart ?GA ?G))))		 Transportation.kif 3987-3997 If X is an instance of transit system, Y is an instance of transitway, the abstract counterpart of X is Z, and X is a system part of Y, then there exists W such that W is an instance of graph arc, the abstract counterpart of Y is W, and W is a part of Z
(=>
    (and
        (instance ?TS TransitSystem)
        (instance ?TJ TransitwayJunction)
        (abstractCounterpart ?G ?TS)
        (systemPart ?TJ ?TS))
    (exists (?GN)
        (and
            (instance ?GN GraphNode)
            (abstractCounterpart ?GN ?TJ)
            (graphPart ?GN ?G))))		 Transportation.kif 3999-4009 If X is an instance of transit system, Y is an instance of transitway junction, the abstract counterpart of X is Z, and X is a system part of Y, then there exists W such that W is an instance of graph node, the abstract counterpart of Y is W, and W is a part of Z
(=>
    (and
        (instance ?SYSTEM TransitSystem)
        (systemPart ?PART ?SYSTEM))
    (instance ?PART Transitway))		 Transportation.kif 4019-4023 If X is an instance of transit system and X is a system part of Y, then Y is an instance of transitway

consequent
-------------------------


(=>
    (and
        (subSystem ?SUB ?SYSTEM)
        (systemPart ?PART ?SUB))
    (systemPart ?PART ?SYSTEM))		 Merge.kif 6261-6265 If X is a sub system of Y and Y is a system part of Z, then X is a system part of Z
(=>
    (routeStart ?R ?TS)
    (exists (?T)
        (and
            (instance ?T Transitway)
            (connected ?R ?T)
            (systemPart ?T ?TS)
            (not
                (exists (?T2)
                    (and
                        (instance ?T2 Transitway)
                        (connected ?R ?T2)
                        (systemPart ?T2 ?TS)
                        (not
                            (equal ?T ?T2))))))))		 Transportation.kif 3901-3915 If X is the start of Y, then All of the following hold: (1) there exists Z such that Z is an instance of transitway (2) X is connected to Z (3) Y is a system part of Z (4) there doesn't exist W such that W is an instance of transitway (5) X is connected to W (6) Y is a system part of W (7) equal Z (8) W
(=>
    (routeEnd ?R ?TS)
    (exists (?T)
        (and
            (instance ?T Transitway)
            (connected ?R ?T)
            (systemPart ?T ?TS)
            (not
                (exists (?T2)
                    (and
                        (instance ?T2 Transitway)
                        (connected ?R ?T2)
                        (systemPart ?T2 ?TS)
                        (not
                            (equal ?T ?T2))))))))		 Transportation.kif 3924-3938 If X is the end of Y, then All of the following hold: (1) there exists Z such that Z is an instance of transitway (2) X is connected to Z (3) Y is a system part of Z (4) there doesn't exist W such that W is an instance of transitway (5) X is connected to W (6) Y is a system part of W (7) equal Z (8) W


Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view)


Sigma web home      Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0.0-0a80e6c8 (2026-05-12) is open source software produced by Articulate Software and its partners