  Gas
|
|
Sigma KEE - subProposition
|
appearance as argument number 1
|
|
|
|
appearance as argument number 2
|
|
|
|
antecedent
|
|
|
(=>
(subProposition ?PROP1 ?PROP2)
(forall (?OBJ1 ?OBJ2)
(=>
(and
(containsInformation ?OBJ1 ?PROP1)
(containsInformation ?OBJ2 ?PROP2))
(subsumesContentInstance ?OBJ2 ?OBJ1)))) |
Merge.kif 4758-4765 |
If X is a sub-proposition of Y, then For all ContentBearingPhysicals Z and W: if Z contains information X and W contains information Y, then W subsumes the content of Z |
(=>
(and
(instance ?X Argument)
(instance ?R Reasoning)
(instance ?A Archeology)
(subProposition ?X ?A)
(realization ?R ?X))
(exists (?D ?S ?O ?T ?W ?L)
(and
(instance ?D Discovering)
(instance ?O Object)
(patient ?D ?O)
(refers ?R ?D)
(earlier
(WhenFn ?D)
(WhenFn ?R))
(age ?O
(MeasureFn ?T YearDuration))
(greaterThan ?T 50)
(holdsDuring
(ImmediatePastFn
(WhenFn ?D))
(or
(and
(surface ?S ?W)
(instance ?W BodyOfWater)
(orientation ?O ?S Below))
(and
(surface ?S ?L)
(instance ?L LandArea)
(orientation ?O ?S Below))))))) |
Geography.kif 6008-6038 |
If X is an instance of argument, Y is an instance of reasoning, Z is an instance of archeology, X is a sub-proposition of Z, and Y expresses the content of X, then there exist W, V,, , U,, , T,, , S and R such that W is an instance of discovering and U is an instance of object and U is a patient of W and Y includes a reference to W and the time of existence of W happens earlier than the time of existence of Y and the age of U is T year duration(s) and T is greater than 50 and V is a surface of S and S is an instance of body of water and U is below to V or V is a surface of R and R is an instance of land area and U is below to V holds during immediately before the time of existence of W |
(=>
(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)) |
Government.kif 745-754 |
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 |
(=>
(and
(instance ?CORPUS RegionalLaw)
(subProposition ?PART ?CORPUS))
(attribute ?CORPUS Law)) |
Government.kif 846-850 |
If X is an instance of regional law and Y is a sub-proposition of X, then law is an attribute of X |
(=>
(subProposition UniversalSuffrageLaw
(RegionalLawFn ?POLITY))
(forall (?AGENT ?ELECTION ?VOTINGAGE ?AGE)
(=>
(and
(citizen ?AGENT ?POLITY)
(suffrageAgeMinimum ?POLITY
(MeasureFn ?VOTINGAGE YearDuration))
(age ?AGENT
(MeasureFn ?AGE YearDuration))
(greaterThanOrEqualTo ?AGE ?VOTINGAGE)
(instance ?ELECTION
(ElectionFn ?POLITY)))
(capability
(VotingFn ?ELECTION) agent ?AGENT)))) |
Government.kif 1077-1089 |
If universal suffrage law is a sub-proposition of the regional law of X, then For all Human Y, Election Z, and RealNumbers W and V: if Y is a citizen of X, W year duration(s) is a suffrage age minimum of X, the age of Y is V year duration(s), V is greater than or equal to W, and Z is an instance of the election of X, then Y is capable of doing the voting of Z as a agent |
(=>
(and
(subProposition UniversalSuffrageLaw
(RegionalLawFn ?POLITY))
(citizen ?AGENT ?POLITY)
(suffrageAgeMinimum ?POLITY
(MeasureFn ?VOTINGAGE YearDuration))
(age ?AGENT
(MeasureFn ?AGE YearDuration))
(greaterThanOrEqualTo ?AGE ?VOTINGAGE)
(instance ?ELECTION
(ElectionFn ?POLITY)))
(capability
(VotingFn ?ELECTION) agent ?AGENT)) |
Government.kif 1091-1101 |
If All of the following hold: (1) universal suffrage law is a sub-proposition of the regional law of X (2) Y is a citizen of X (3) Z year duration(s) is a suffrage age minimum of X (4) the age of Y is W year duration(s) (5) W is greater than or equal to Z (6) V is an instance of the election of X, then Y is capable of doing the voting of V as a agent |
(=>
(and
(subProposition ExclusiveMaleSuffrage
(RegionalLawFn ?POLITY))
(citizen ?AGENT ?POLITY)
(instance ?ELECTION
(ElectionFn ?POLITY))
(capability
(VotingFn ?ELECTION) agent ?AGENT))
(attribute ?AGENT Male)) |
Government.kif 1221-1227 |
If exclusive male suffrage is a sub-proposition of the regional law of X, Y is a citizen of X, Z is an instance of the election of X, and Y is capable of doing the voting of Z as a agent, then male is an attribute of Y |
(=>
(and
(subProposition ExclusiveMaleSuffrage
(RegionalLawFn ?POLITY))
(citizen ?AGENT ?POLITY)
(instance ?ELECTION
(ElectionFn ?POLITY))
(instance ?ACT
(VotingFn ?ELECTION))
(agent ?ACT ?AGENT))
(attribute ?AGENT Male)) |
Government.kif 1229-1236 |
If exclusive male suffrage is a sub-proposition of the regional law of X, Y is a citizen of X, Z is an instance of the election of X, W is an instance of the voting of Z, and Y is an agent of W, then male is an attribute of Y |
(=>
(and
(subProposition ExclusiveMaleSuffrage
(RegionalLawFn ?AREA))
(attribute ?AGENT Female)
(member ?AGENT
(ResidentFn ?AREA))
(instance ?ELECTION Election))
(not
(capability
(VotingFn ?ELECTION) agent ?AGENT))) |
Government.kif 1238-1244 |
If exclusive male suffrage is a sub-proposition of the regional law of X, female is an attribute of Y, Y is a member of the resident of X, and Z is an instance of election, then Y is not capable of doing the voting of Z as a agent |
|
consequent
|
|
|
(=>
(instance ?L LyricalContent)
(exists (?W ?I)
(and
(instance ?W Word)
(containsInformation ?W ?I)
(subProposition ?I ?L)))) |
Mid-level-ontology.kif 15397-15403 |
If X is an instance of lyrical content, then there exist Y, Z such that Y is an instance of word, Y contains information Z, and Z is a sub-proposition of X |
(=>
(instance ?API ApplicationProgrammerInterface)
(exists (?P)
(and
(instance ?P ComputerProgram)
(subProposition ?API ?P)))) |
ComputingBrands.kif 1929-1934 |
If X is an instance of Application Programmer Interface, then there exists Y such that Y is an instance of computer program and X is a sub-proposition of Y |
(=>
(instance ?CONST Constitution)
(exists (?FORMULA ?PART)
(and
(instance ?FORMULA Formula)
(containsFormula ?PART ?FORMULA)
(instance ?PART Proposition)
(subProposition ?PART ?CONST)
(modalAttribute ?FORMULA Obligation)))) |
Government.kif 617-625 |
If X is an instance of constitution, then there exist Y, Z such that Y is an instance of formula, Z contains the formula Y, Z is an instance of proposition, Z is a sub-proposition of X, and the statement Y has the modal force of obligation |
(=>
(instance ?CONST Constitution)
(exists (?FORMULA ?PART)
(and
(instance ?FORMULA Formula)
(containsFormula ?PART ?FORMULA)
(instance ?PART Proposition)
(subProposition ?PART ?CONST)
(modalAttribute ?FORMULA Permission)))) |
Government.kif 627-635 |
If X is an instance of constitution, then there exist Y, Z such that Y is an instance of formula, Z contains the formula Y, Z is an instance of proposition, Z is a sub-proposition of X, and the statement Y has the modal force of permission |
(=>
(agreementRevisionDate ?AGR ?DATE ?CHANGE)
(exists (?TIME)
(and
(instance ?TIME ?DATE)
(or
(and
(holdsDuring
(ImmediatePastFn ?TIME)
(not
(subProposition ?CHANGE ?AGR)))
(holdsDuring
(ImmediateFutureFn ?TIME)
(subProposition ?CHANGE ?AGR)))
(and
(holdsDuring
(ImmediatePastFn ?TIME)
(subProposition ?CHANGE ?AGR))
(holdsDuring
(ImmediateFutureFn ?TIME)
(not
(subProposition ?CHANGE ?AGR)))))))) |
Government.kif 705-726 |
If X agreement revision date Y for Z, then there exists W such that W is an instance of Y, Z is not a sub-proposition of X holds during immediately before W, Z is a sub-proposition of X holds during immediately after W or Z is a sub-proposition of X holds during immediately before W, and Z is not a sub-proposition of X holds during immediately after W |
(=>
(and
(instance ?COUNTRY Nation)
(governmentType ?COUNTRY Democracy))
(exists (?SUFFRAGE)
(and
(instance ?SUFFRAGE SuffrageLaw)
(subProposition ?SUFFRAGE
(RegionalLawFn ?COUNTRY))))) |
Government.kif 877-884 |
If X is an instance of nation and democracy is a government type of X, then there exists Y such that Y is an instance of suffrage law and Y is a sub-proposition of the regional law of X |
(=>
(and
(instance ?COUNTRY GeopoliticalArea)
(governmentType ?COUNTRY Democracy))
(subProposition VoterCitizenshipRequirement
(RegionalLawFn ?COUNTRY))) |
Government.kif 888-892 |
If X is an instance of geopolitical area and democracy is a government type of X, then voter citizenship requirement is a sub-proposition of the regional law of X |
(=>
(instance ?COUNTRY Nation)
(exists (?AGERULE)
(and
(instance ?AGERULE VoterAgeRequirement)
(subProposition ?AGERULE
(RegionalLawFn ?COUNTRY))))) |
Government.kif 906-911 |
If X is an instance of nation, then there exists Y such that Y is an instance of voter age requirement and Y is a sub-proposition of the regional law of X |
(=>
(instance ?X TravelReservation)
(modalAttribute
(exists (?FLIGHT)
(and
(instance ?FLIGHT FlightReservation)
(subProposition ?FLIGHT ?X))) Likely)) |
Hotel.kif 2842-2848 |
If X is an instance of travel reservation, then the statement there exists Y such that Y is an instance of flight reservation and Y is a sub-proposition of X has the modal force of likely |
(=>
(equal ?M
(MusicalComponentFn ?S))
(subProposition ?M ?S)) |
Music.kif 910-912 |
If equal X and the music of Y, then X is a sub-proposition of Y |
(=>
(equal ?L
(LyricalComponentFn ?S))
(subProposition ?L ?S)) |
Music.kif 922-924 |
If equal X and the lyrics of Y, then X is a sub-proposition of Y |
|
Show simplified definition (without tree view)
Show simplified definition (with tree view)
|
