Browsing Interface : Welcome guest : log in
Home |  Graph |  ]  KB:  Language:   

Formal Language: 



KB Term:  Term intersection
English Word: 

Sigma KEE - subProposition
subProposition

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


s__documentation(s__subProposition__m,s__ChineseLanguage,'"(subProposition ?PROP1 ?PROP2) 的意思是 ?PROP1 是一个 Proposition,它是 Proposition ?PROP2 的一个真正部分。换句话说 subProposition 是一堆抽象内容的 properPart 的类似物。"')

chinese_format.kif 2203-2205
s__documentation(s__subProposition__m,s__EnglishLanguage,'"(subProposition ?PROP1 ?PROP2) means that ?PROP1 is a Proposition which is a proper part of the Proposition ?PROP2. In other words, subProposition is the analogue of properPart for chunks of abstract content."')

Merge.kif 4500-4503
s__domain(s__subProposition__m,n__1,s__Proposition)

Merge.kif 4497-4497 The number 1 argument of sub proposition is an instance of proposition
s__domain(s__subProposition__m,n__2,s__Proposition)

Merge.kif 4498-4498 The number 2 argument of sub proposition is an instance of proposition
s__instance(s__subProposition__m,s__BinaryPredicate)

s__instance(s__BinaryPredicate,s__SetOrClass)

Merge.kif 4493-4493 sub proposition is an instance of binary predicate
s__instance(s__IrreflexiveRelation,s__SetOrClass)

s__instance(s__subProposition__m,s__IrreflexiveRelation)

Merge.kif 4495-4495 sub proposition is an instance of irreflexive relation
s__instance(s__PartialValuedRelation,s__SetOrClass)

s__instance(s__subProposition__m,s__PartialValuedRelation)

Merge.kif 4496-4496 sub proposition is an instance of partial valued relation
s__instance(s__TransitiveRelation,s__SetOrClass)

s__instance(s__subProposition__m,s__TransitiveRelation)

Merge.kif 4494-4494 sub proposition is an instance of transitive relation

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


s__format(s__ChineseLanguage,s__subProposition__m,'"%1 %n 是 %2 的 subProposition"')

chinese_format.kif 187-187
s__format(s__EnglishLanguage,s__subProposition__m,'"%1 is %n a sub-proposition of %2"')

english_format.kif 191-191
s__subrelation(s__subField__m,s__subProposition__m)

Mid-level-ontology.kif 20306-20306 sub field is a subrelation of sub proposition
s__subrelation(s__subPlan__m,s__subProposition__m)

Merge.kif 4514-4514 sub plan is a subrelation of sub proposition
s__termFormat(s__ChineseLanguage,s__subProposition__m,'"子命题"')

chinese_format.kif 188-188
s__termFormat(s__ChineseLanguage,s__subProposition__m,'"次提案"')

domainEnglishFormat.kif 55761-55761
s__termFormat(s__ChineseTraditionalLanguage,s__subProposition__m,'"次提案"')

domainEnglishFormat.kif 55760-55760
s__termFormat(s__EnglishLanguage,s__subProposition__m,'"sub proposition"')

domainEnglishFormat.kif 55759-55759

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


No TPTP formula. May not be expressible in strict first order. Government.kif 1118-1138
No TPTP formula. May not be expressible in strict first order. Government.kif 761-769
( ! [V__CORPUS,V__PART] :
   ((s__instance(V__PART,s__Proposition) =>
       (((s__instance(V__CORPUS,s__RegionalLaw) &
             s__subProposition(V__PART,V__CORPUS))
         =>
         (s__attribute(V__CORPUS,s__Law)))))
   )
)

Government.kif 861-865
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 20128-20157
( ! [V__AGENT,V__POLITY,V__AGE,V__VOTINGAGE,V__ELECTION] :
   (((s__instance(V__AGENT,s__Human) &
         s__instance(V__POLITY,s__Nation) &
         s__instance(V__AGE,s__RealNumber) &
         s__instance(V__VOTINGAGE,s__RealNumber) &
         s__instance(V__ELECTION,s__Election))
       =>
       (((s__subProposition(s__CompulsorySuffrageLaw,s__RegionalLawFn(V__POLITY))
         &
         s__citizen(V__AGENT,V__POLITY)
       &
       s__suffrageAgeMinimum(V__POLITY,s__MeasureFn(V__VOTINGAGE,s__YearDuration))
     &
     s__age(V__AGENT,s__MeasureFn(V__AGE,s__YearDuration))
   &
   s__greaterThanOrEqualTo(V__AGE,V__VOTINGAGE)
&
s__instance(V__ELECTION,s__ElectionFn(V__POLITY)))
=>
(( ? [V__VOTING] :
((s__instance(V__VOTING,s__Process) &
   (s__instance(V__VOTING,s__VotingFn(V__ELECTION))
&
s__agent(V__VOTING,V__AGENT)))))))))
)
)

Government.kif 1162-1175
No TPTP formula. May not be expressible in strict first order. Government.kif 1197-1217
( ! [V__AGENT,V__AREA,V__ELECTION] :
   (((s__instance(V__AGENT,s__Object) &
         s__instance(V__AREA,s__GeopoliticalArea))
       =>
       (((s__subProposition(s__ExclusiveMaleSuffrage,s__RegionalLawFn(V__AREA))
         &
         s__attribute(V__AGENT,s__Female) &
         s__member(V__AGENT,s__ResidentFn(V__AREA))
     &
     s__instance(V__ELECTION,s__Election))
   =>
   (~(s__capability(s__VotingFn(V__ELECTION)
    ,s__agent__m,V__AGENT))))))
)
)

Government.kif 1253-1259
( ! [V__AGENT,V__POLITY,V__ELECTION] :
   (((s__instance(V__AGENT,s__Human) &
         s__instance(V__POLITY,s__Nation) &
         s__instance(V__ELECTION,s__Election))
       =>
       (((s__subProposition(s__ExclusiveMaleSuffrage,s__RegionalLawFn(V__POLITY))
         &
         s__citizen(V__AGENT,V__POLITY)
       &
       s__instance(V__ELECTION,s__ElectionFn(V__POLITY))
   &
   s__capability(s__VotingFn(V__ELECTION)
,s__agent__m,V__AGENT))
=>
(s__attribute(V__AGENT,s__Male)))))
)
)

Government.kif 1236-1242
( ! [V__AGENT,V__POLITY,V__ACT,V__ELECTION] :
   (((s__instance(V__AGENT,s__Human) &
         s__instance(V__POLITY,s__Nation) &
         s__instance(V__ACT,s__Process) &
         s__instance(V__ELECTION,s__Election))
       =>
       (((s__subProposition(s__ExclusiveMaleSuffrage,s__RegionalLawFn(V__POLITY))
         &
         s__citizen(V__AGENT,V__POLITY)
       &
       s__instance(V__ELECTION,s__ElectionFn(V__POLITY))
   &
   s__instance(V__ACT,s__VotingFn(V__ELECTION))
&
s__agent(V__ACT,V__AGENT))
=>
(s__attribute(V__AGENT,s__Male)))))
)
)

Government.kif 1244-1251
( ! [V__AGENT,V__POLITY,V__AGE,V__VOTINGAGE,V__ELECTION] :
   (((s__instance(V__AGENT,s__Human) &
         s__instance(V__POLITY,s__Nation) &
         s__instance(V__AGE,s__RealNumber) &
         s__instance(V__VOTINGAGE,s__RealNumber) &
         s__instance(V__ELECTION,s__Election))
       =>
       (((s__subProposition(s__UniversalSuffrageLaw,s__RegionalLawFn(V__POLITY))
         &
         s__citizen(V__AGENT,V__POLITY)
       &
       s__suffrageAgeMinimum(V__POLITY,s__MeasureFn(V__VOTINGAGE,s__YearDuration))
     &
     s__age(V__AGENT,s__MeasureFn(V__AGE,s__YearDuration))
   &
   s__greaterThanOrEqualTo(V__AGE,V__VOTINGAGE)
&
s__instance(V__ELECTION,s__ElectionFn(V__POLITY)))
=>
(s__capability(s__VotingFn(V__ELECTION)
,s__agent__m,V__AGENT)))))
)
)

Government.kif 1106-1116
( ! [V__PROP1,V__PROP2] :
   (((s__instance(V__PROP1,s__Proposition) &
         s__instance(V__PROP2,s__Proposition))
       =>
       ((s__subProposition(V__PROP1,V__PROP2)
         =>
         (( ! [V__OBJ1, V__OBJ2] :
             (((s__instance(V__OBJ1,s__ContentBearingPhysical) &
                   s__instance(V__OBJ2,s__ContentBearingPhysical))
                 =>
                 (((s__containsInformation(V__OBJ1,V__PROP1)
                     &
                     s__containsInformation(V__OBJ2,V__PROP2))
                 =>
                 (s__subsumesContentInstance(V__OBJ2,V__OBJ1)))))))))))
)
)

Merge.kif 4505-4512
No TPTP formula. May not be expressible in strict first order. Government.kif 1177-1195
( ! [V__POLITY] :
   ((s__instance(V__POLITY,s__Nation) =>
       ((s__subProposition(s__UniversalSuffrageLaw,s__RegionalLawFn(V__POLITY))
       =>
       (( ! [V__AGENT, V__ELECTION, V__VOTINGAGE, V__AGE] :
           (((s__instance(V__AGENT,s__Human) &
                 s__instance(V__ELECTION,s__Election) &
                 s__instance(V__VOTINGAGE,s__RealNumber) &
                 s__instance(V__AGE,s__RealNumber))
               =>
               (((s__citizen(V__AGENT,V__POLITY)
                   &
                   s__suffrageAgeMinimum(V__POLITY,s__MeasureFn(V__VOTINGAGE,s__YearDuration))
                 &
                 s__age(V__AGENT,s__MeasureFn(V__AGE,s__YearDuration))
               &
               s__greaterThanOrEqualTo(V__AGE,V__VOTINGAGE)
             &
             s__instance(V__ELECTION,s__ElectionFn(V__POLITY)))
       =>
       (s__capability(s__VotingFn(V__ELECTION)
      ,s__agent__m,V__AGENT)))))))))))
)
)

Government.kif 1092-1104

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


No TPTP formula. May not be expressible in strict first order. Government.kif 725-740
No TPTP formula. May not be expressible in strict first order. Government.kif 1015-1024
No TPTP formula. May not be expressible in strict first order. Government.kif 943-952
( ! [V__ARGUMENT,V__PREMISES,V__PROPOSITION] :
   (((s__instance(V__PREMISES,s__Proposition) &
         s__instance(V__PROPOSITION,s__Proposition))
       =>
       (((s__instance(V__ARGUMENT,s__Argument) &
             (V__PREMISES = s__PremisesFn(V__ARGUMENT)))
         =>
         (((s__subProposition(V__PROPOSITION,V__PREMISES)
             =>
             s__premise(V__ARGUMENT,V__PROPOSITION))
         &
         (s__premise(V__ARGUMENT,V__PROPOSITION)
         =>
         s__subProposition(V__PROPOSITION,V__PREMISES)))))))
)
)

Merge.kif 16204-16210
( ! [V__COUNTRY] :
   (((s__instance(V__COUNTRY,s__GeopoliticalArea) &
         s__governmentType(V__COUNTRY,s__Democracy))
       =>
       (s__subProposition(s__VoterCitizenshipRequirement,s__RegionalLawFn(V__COUNTRY))))
)
)

Government.kif 903-907
( ! [V__COUNTRY] :
   (((s__instance(V__COUNTRY,s__Nation) &
         s__governmentType(V__COUNTRY,s__Democracy))
       =>
       (( ? [V__SUFFRAGE] :
           ((s__instance(V__SUFFRAGE,s__SuffrageLaw) &
               s__subProposition(V__SUFFRAGE,s__RegionalLawFn(V__COUNTRY)))))))
)
)

Government.kif 892-899
( ! [V__S,V__L] :
   (((s__instance(V__S,s__Song) &
         s__instance(V__L,s__LyricalContent))
       =>
       (((V__L = s__LyricalComponentFn(V__S))
         =>
         (s__subProposition(V__L,V__S)))))
)
)

Music.kif 916-918
( ! [V__S,V__M] :
   (((s__instance(V__S,s__Song) &
         s__instance(V__M,s__MusicalComposition))
       =>
       (((V__M = s__MusicalComponentFn(V__S))
         =>
         (s__subProposition(V__M,V__S)))))
)
)

Music.kif 904-906
( ! [V__API] :
   ((s__instance(V__API,s__ApplicationProgrammerInterface) =>
       (( ? [V__P] :
           ((s__instance(V__P,s__ComputerProgram) &
               s__subProposition(V__API,V__P))))))
   )
)

ComputingBrands.kif 1896-1901
No TPTP formula. May not be expressible in strict first order. Government.kif 640-648
No TPTP formula. May not be expressible in strict first order. Government.kif 650-658
( ! [V__COUNTRY] :
   ((s__instance(V__COUNTRY,s__Nation) =>
       (( ? [V__AGERULE] :
           ((s__instance(V__AGERULE,s__VoterAgeRequirement) &
               s__subProposition(V__AGERULE,s__RegionalLawFn(V__COUNTRY)))))))
)
)

Government.kif 921-926
( ! [V__L] :
   ((s__instance(V__L,s__LyricalContent) =>
       (( ? [V__W, V__I] :
           ((s__instance(V__I,s__Proposition) &
               (s__instance(V__W,s__Word) &
                 s__containsInformation(V__W,V__I)
               &
               s__subProposition(V__I,V__L)))))))
)
)

Mid-level-ontology.kif 12993-12999
No TPTP formula. May not be expressible in strict first order. Hotel.kif 2793-2799
No TPTP formula. May not be expressible in strict first order. Mid-level-ontology.kif 13333-13338


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 is open source software produced by Articulate Software and its partners