TreeView Knowledge Base Browser

appearance as argument number 1

(instance ConstitutionFn UnaryFunction)	Government.kif 637-637	Constitution is an instance of unary function
(domain ConstitutionFn 1 GeopoliticalArea)	Government.kif 638-638	The number 1 argument of constitution is an instance of geopolitical area
(rangeSubclass ConstitutionFn Constitution)	Government.kif 639-639	The values returned by constitution are subclasses of constitution
(documentation ConstitutionFn EnglishLanguage "(ConstitutionFn ?AREA) denotes a class containing all Constitutions adopted by the government of the GeopoliticalArea ?AREA. For example, (ConstitutionFn UnitedStates) contains the ConstitutionOfTheUnitedStates.")	Government.kif 641-644	The values returned by constitution are subclasses of constitution

appearance as argument number 2

(format EnglishLanguage ConstitutionFn "the constitution of %1")	domainEnglishFormat.kif 538-538
(format ChineseTraditionalLanguage ConstitutionFn "%1 的 constitution ")	domainEnglishFormat.kif 539-539
(format ChineseLanguage ConstitutionFn "%1 的 constitution ")	domainEnglishFormat.kif 540-540
(termFormat EnglishLanguage ConstitutionFn "constitution")	domainEnglishFormat.kif 16776-16776
(termFormat ChineseTraditionalLanguage ConstitutionFn "憲法")	domainEnglishFormat.kif 16777-16777
(termFormat ChineseLanguage ConstitutionFn "宪法")	domainEnglishFormat.kif 16778-16778

antecedent

(=>
    (and
        (instance ?CONST
            (ConstitutionFn ?COUNTRY))
        (instance ?COUNTRY Nation)
        (equal ?GOV
            (GovernmentFn ?COUNTRY))
        (instance
            (WhenFn ?GOV) ?CLASS)
        (agreementEffectiveDuring ?CONST ?CLASS)
        (subProposition ?PART ?CONST)
        (containsFormula ?PART ?FORMULA))
    (holdsObligation ?GOV ?FORMULA))

If All of the following hold: (1) X is an instance of the constitution of Y (2) Y is an instance of nation (3) equal Z and the government of Y (4) the time of existence of Z is an instance of W (5) W is an agreement effective during of X (6) V is a sub-proposition of X (7) V contains the formula U, then Z is obliged to perform tasks of type U