13.1. Conditional Queries
The terminology used in this document to refer to different types of queries is:

 “ASK” > Generalpurpose query
 “PROVE” > Conditional query
 “QUERY” > Could be either of the above
They will be used in all capitals to distingish them from the common usage of these words.
Before explaining conditional queries, some explanation of Cyc’s generalpurpose inference mechanism is required.
13.1.1. Generalpurpose queries (ASK)
The functionality of Cyc’s generalpurpose inference mechanism is focused on generating unique proofs that sets of closed terms unify with the free variables of a query. This is an ASK.
For example, ASKing the query
(geopoliticalSubdivision Canada ?WHAT) in #$WorldGeographyMt
is a request to generate sets of bindings for the free variables such as the following
((?WHAT . ManitobaCanadianProvince))
along with a complete deductive justification for each one. In the Cyc Browser, the binding sets are presented as a table, with the columns being the free variables.
ASKing
(thereExists ?WHAT (geopoliticalSubdivision Canada ?WHAT)) in #$WorldGeographyMt
results in an identical proof being performed except that, by convention, the bindings for a successful proof are given as
((T . T))
since there are no free variables. Each potential binding for ?WHAT is part of an independent justification for the fact that there exist any at all. ((T . T)) is displayed in the Cyc Browser as “Query was proven True”.
In short, all free variables in an ASK have an implicit existential quantification wrapped around them for purposes of resolving the ambiguity. Those variables that are free in the original query are interpreted as being those for which bindings are requested that indeed prove the existence of such terms satisfying the query.
13.1.2. ASKing disjunctive queries
ASKing disjunctive queries like
(or (isa ?WHAT CanadianProvince) (geopoliticalSubdivision Canada ?WHAT)) in #$WorldGeographyMt
is a request to generate bindings that either satisfy
(isa ?WHAT CanadianProvince)
or
(geopoliticalSubdivision Canada ?WHAT)
Now consider a slightly different disjunctive query :
(or (not (isa ?WHAT CanadianProvince)) (geopoliticalSubdivision Canada ?WHAT)) in #$WorldGeographyMt
This is logically equivalent to the query
(implies (isa ?WHAT CanadianProvince) (geopoliticalSubdivision Canada ?WHAT)) in #$WorldGeographyMt
ASKing either of these forms of the query is a request to return bindings for ?WHAT that satisfy this disjunction. Note that
((?WHAT . EiffelTower))
satisfies this disjunction since it is not a Canadian province.
13.1.3. Conditional Queries (PROVE)
It would be more interesting to be able to ask a conditional query in which ?WHAT is universally quantified, rather than existentially quantified, as in :
;; Is every Canadian province a political subdivision of Canada? (forAll ?WHAT (implies (isa ?WHAT CanadianProvince) (geopoliticalSubdivision Canada ?WHAT))) in #$WorldGeographyMt
PROVE is a mechanism designed to provide support for this kind of conditional query. It accepts formulas of the exact syntactic form
(implies <ANTECEDENT> <CONSEQUENT>) in <MT>
Any <SENTENCE> not of this exact syntactic form is treated as if
(implies True <SENTENCE>)
were provided.
Unlike ASK, the free variables of the antecedent (if any) are assumed universally quantified for the entire query. The remaining free variables of the consequent (if any) are then assumed existentially quantified around that.
In order to prove the universal quantifications, PROVE creates a hypothetical microtheory (the “hypothesis mt”) and hypothetical terms for each of the free variables of the antecedent, and assumes the antecedent is true of the hypothetical terms in the hypothesis mt. The hypothesis mt has the query <MT> of the PROVE as its sole genlMt. The hypothesis microtheory therefore represents a possible world in which the antecedent condition is assumed true of generic terms.
We then create another hypothetical microtheory (the “proof mt”) for the further type constraints on the generic terms which are imposed by the consequent within the possible world of the antecedent being true. The proof microtheory therefore represents a possible world in which the antecedent and the type constraints from the consequent are assumed true of generic terms.
Within the possible world of the proof microtheory, we then perform an ASK of the consequent with the generic terms substituted for the free variables appearing in the antecedent. If any proof can then be found, by the rule of universal generalization, it is a proof of the universals since they were arbitrarily chosen.
In short, PROVE creates
 two nested possible worlds, one that assumes the antecedent and one that assumes the antecedent plus additional type constraints from the consequent
 generic terms for free variables in the antecedent which satisfy the antecedent in these possible worlds
It then does a normal ASK in these possible worlds, where an answer would prove a logically equivalent universal result in the query context.
13.1.4. The Cyc Browser’s QUERY tool
The Cyc Browser’s QUERY tool (labeled “Ask” or “Ask A Query”) is a wrapper around both ASK and PROVE. Any query of the syntactic form
(implies <antecedent> <consequent>)
is passed off to PROVE, since that is usually what is intended. All other queries are passed to ASK.
13.1.5. Tautologies and Contradictions in ASK
In ASK, certain logical tautologies like
(or (geopoliticalSubdivision Canada ?WHAT) (not (geopoliticalSubdivision Canada ?WHAT)))
can be detected automatically by the canonicalizer, which reduces them to #$True. In this case, no inference is performed and
((T . T)) :TAUTOLOGY
is returned by ASK, indicating that the query was logically a tautology. In the Cyc Browser, this displays as “Query reduced to True (a tautology).” Similarly, a logical contradiction like
(and (geopoliticalSubdivision #$Canada ?WHAT) (not (geopoliticalSubdivision Canada ?WHAT)))
can be detected and reduced to #$False by the canonicalizer. In this case, no inference is performed and
NIL :CONTRADICTION
is returned. This displays as “Query reduced to False (a contradiction).”.
13.1.6. Tautologies and Contradictions in PROVE
Since PROVE accepts formulas of the form
(implies <ANTECEDENT> <CONSEQUENT>)
if the <ANTECEDENT> ever reduced to #$False, the entire proof would reduce to #$True. Therefore, if the antecedent is unsatisfiable in the possible world of the hypothesis mt, PROVE returns
((T . T)) :TAUTOLOGY
If the additional constraints of the consequent are unsatisfiable in the possible world of the proof mt, PROVE likewise returns
((T . T)) :TAUTOLOGY
Finally, since the consequent formula is passed to ASK in the proof mt, if it reduces to #$True or #$False there, PROVE returns either
((T . T)) :TAUTOLOGY NIL :CONTRADICTION
13.1.7. Detailed Example
Assume we want to ask the following query :
;; Is every Canadian province a political subdivision of Canada? (forAll ?WHAT (implies (isa ?WHAT CanadianProvince) (geopoliticalSubdivision Canada ?WHAT))) in #$WorldGeographyMt
We call PROVE with
(implies (isa ?WHAT CanadianProvince) (geopoliticalSubdivision Canada ?WHAT))) in #$WorldGeographyMt
This causes an instance of #$HypotheticalContext to be created
(isa #$HYPContext001 HypotheticalContext) (genlMt HYPContext001 WorldGeographyMt)
It then creates a hypothetical Canadian province in that world :
In Mt : HYPContext001 (isa HYPProvince001 CanadianProvince)
We create a proof microtheory:
(isa HYPContext002 HypotheticalContext) (genlMt HYPContext002 HYPContext001)
Here we additionally assume
In Mt : #$HYPContext002 (isa #$HYPProvince001 GeopoliticalEntity)
We then do an ASK of
(geopoliticalSubdivision Canada HYPProvince001) in #$HYPContext002
If this can be proven of our generic province in this possible world, it can be proven of every province in WorldGeographyMt.
13.1.8. Caching of hypothesis microtheories
The advantage of separating the hypothesis mt from the query mt is clear; it allows us to reason about a possible world without modifying the context on which that world is based.
The advantage of separating the hypothesis mt from the proof mt is that several different proofs that assume the same possible world can reuse that world for different proofs.
For example, using PROVE on
;; Every Canadian province is a political subdivision of what country? (implies (isa ?WHAT CanadianProvince) (and (isa ?COUNTRY Country) (geopoliticalSubdivision ?COUNTRY ?WHAT))) in #$WorldGeographyMt
assuming we already did the earlier proof, we can reuse the possible world
#$HYPContext001
since this query uses the same assumed antecedent. We then only have to create a different proof mt, in which we ASK
(and (isa ?COUNTRY Country) (geopoliticalSubdivision ?COUNTRY HYPProvince001))
in #$HYPContext003
in which we should be able to return
((?COUNTRY . Canada))
as a binding.
Currently, we do not reuse proof mts, although this extension would be a natural one to make.
13.1.9. Ephemerality of possible worlds and hypothesized terms
All the terms hypothesised by PROVE, including
 hypothesis mts
 proof mts
 generic terms
are all marked as #$ephemeralTerm, indicating that they are internal to this particular Cyc image. Furthermore we use #$termDependsOn and #$definingMt to indicate the mutual dependence of these terms on the hypothesis mt and the original query mt. Therefore, if the original query mt were killed, all these hypothesized terms would automatically be killed as well.
13.1.10. More on type constraints
The assumption in the proof mt of the additional constraints from the consequent makes PROVE’s interpretation of typeconstraints identical to that of the inference engine’s in regard to the application of rules.
Thus, if the assert
ASSERT (implies P(x) Q(x)) in MT
is accepted by the system, asking afterward
PROVE (implies P(x) Q(x)) in MT, backchain = 1
should now always succeed, even if the type constraints on x due to Q(x) are stronger than those due to P(x).
13.1.11. Antecedent syntactic restrictions in PROVE
The antecedent of an PROVE has additional syntactic restrictions. Since it specifies a formula which is intended to be made true in a possible world, the creation of generic terms for the free variables is much like the creation of new concepts followed by the asserting sentences about those concepts.
Because we want to reject possible worlds in which the antecedent is unsatisfiable, or leads to contradictions, we want to use something like WFF constraints to reject as unsatisfiable an antecedent like
(and (isa ?CAR Automobile) (feelsEmotion ?CAR Happiness Positive))
since it is nonsensical for a car to be the arg1 of a feelsEmotion assertion. However, just using the same WFF constraints that we use during an assert could lead to problems in this case:
(and (isa ?MOM AdultPerson) (mother Napoleon ?MOM))
In this case, the mother literal imposes a #$FemalePerson constraint which is orthogonal to the #$AdultPerson constraint on ?MOM. So, we can’t simply create an adult person and assert the #$mother literal because the ?MOM would not yet be known to be a #$FemalePerson.
Instead, we analyze the entire antecedent to gather all the type constraints, both #$isa and #$genls, on the free variables and first assert all of these. If this succeeds, we then try asserting all the remaining assumptions, in order listed in the antecedent.
13.2. Using thereExists To Eliminate Unwanted Variables
If you are asking a query in Cyc, it will give you bindings for every free variable in the query. If you don’t care about bindings for a particular variable, you can existentially quantify that variable so the system won’t return bindings for it.
Example: Say that we wanted to ask Cyc for all the redheaded men with children. If we ask
(#$and (#$isa ?MAN #$AdultMalePerson) (#$hairColor ?MAN #$Scalp #$RedColor) (#$children ?MAN ?KID))
Then we will get back bindings for both variables, ?MAN and ?KID. But if we really only want to know about the redheaded men with children, and don’t care about their children, then we could ask this instead:
(#$thereExists ??KID (#$and (#$isa ?MAN #$AdultMalePerson) (#$hairColor ?MAN #$Scalp #$RedColor) (#$children ?MAN ??KID)))
By wrapping a #$thereExists ?KID around the query, Cyc will now know that you only care about the existence of bindings for that variable and that you don’t care about the bindings themselves. Note the ?? prefix on ??KID. This is a convention that indicates the variable is a “don’t care” variable. It is not currently (August 2001) used by Cyc except for certain diagnostic utilities.
13.3. Using assertedSentence etc. To Block Unwanted Inheritance
The transitivity support in the inference engine is very powerful, but sometimes you are looking only for things that have been explicitly asserted, not those which can be inferred. There are some HLsupported predicates you can use to specify this. They are:
 #$assertedSentence
 #$istAsserted
 #$assertedPredicateArg
13.3.1. #$assertedSentence
Here is an example of a case where #$assertedSentence comes in handy.
Imagine that you wanted to find all of the binary relations in the KB that could take an instance of #$Missile in one or more argument positions. You might try the query
(thereExists ??N (thereExists ?WHAT (and (isa ?RELN BinaryPredicate) (argIsa ?RELN ??N ?WHAT) (genls Missile ?WHAT))))
[also see the section “Using thereExists To Eliminate Unwanted Variables” in this chapter]
You might be surprised to see that many of the predicates returned from this query would be such that neither of the argIsas was a generalization of #$Missile, e.g. #$lockState, which relates an instance of #$Lock to an instance of #$LockStateAttribute.
This is because Cyc believes
(transitiveViaArg argIsa genls 3)
Hence, since Cyc knows
(argIsa lockState 1 Lock)
it can conclude from the above two assertions:
(argIsa lockState 1 PartiallyTangible)
and since #$PartiallyTangible is a genls of #$Missile, back comes #$lockState in the binding list for ?RELN.
This is a case in which you would want to use #$assertedSentence to block unwanted inheritance. Instead of the initial query
(thereExists ??N (thereExists ?WHAT (and (isa ?RELN BinaryPredicate) (argIsa ?RELN ??N ?WHAT) (genls Missile ?WHAT))))
the following query will get you the answers you seek:
(thereExists ??N (thereExists ?WHAT (and (isa ?RELN BinaryPredicate) (assertedSentence (argIsa ?RELN ??N ?WHAT)) (genls Missile ?WHAT))))
The only obscure case that the above query would not cover is if there were a predicate which had disjoint arg constraints, one of which was a spec of #$Missile. There are diagnostics which should catch this OE error, but if you wanted to eliminate such relations from coming back as bindings for ?RELN, you could modify the query thusly:
(thereExists ?N (thereExists ?WHAT (and (isa ?RELN BinaryPredicate) (assertedSentence (argIsa ?RELN ?N ?WHAT)) (unknownSentence (thereExists ?OTRWHAT (and (argIsa ?RELN ?N ?OTRWHAT) (disjointWith ?OTRWHAT Missile)))) (genls Missile ?WHAT))))
Another predicate related to #$assertedSentence is #$assertionSentence. It is related in the following way:
(#$assertedSentence :SENTENCE)
is equivalent to
(#$thereExists ?ASSERTION (#$assertionSentence ?ASSERTION :SENTENCE))
13.3.2. #$assertedPredicateArg
Say that you wanted to see whether there was a #$capitalCity assertion for the United States. You don’t want to know whether Cyc can infer the United States’ capital city, and you don’t care what it is; you just want to know whether there is currently an actual assertion of the form (#$capitalCity #$UnitedStatesOfAmerica <whatever>). To ask this query you can use #$assertedPredicateArg as follows:
(#$assertedPredicateArg #$UnitedStatesOfAmerica 1 #$capitalCity)
We could have also asked
(#$thereExists ?CITY (#$assertedSentence (#$capitalCity #$UnitedStatesOfAmerica ?CITY)))
to get the same result.
Hence, #$assertedPredicateArg is just shorthand for a common case of #$assertedSentence; wrapping a bunch of existentials around the arguments you don’t care about, and saving you from worrying about the arity of the predicate. It’s most useful when you don’t know the predicate or the argument number at query construction time, because it would be nigh impossible to write a terse query to achieve the effect of #$assertedPredicateArg.
(#$assertedPredicateArg :TERM 1 :PRED)
is equivalent to
(#$thereExists ?RESTARGS (#$assertedSentence (:PRED :TERM . ?RESTARGS)))
and similarly,
(#$assertedPredicateArg :TERM 2 :PRED)
is equivalent to
(#$thereExists ?ARG1 (#$thereExists ?RESTARGS (#$assertedSentence (:PRED ?ARG1 :TERM . ?RESTARGS))))
etc.
13.3.3. #$istAsserted
#$istAsserted is like a version of #$assertedSentence which gives you control over the microtheory assumptions.
This is most useful when you don’t know the microtheory at query construction time. It’s good for reasoning in one context about whether something’s asserted in another context.
Say you want to find all the specs of #$Fruit in the #$BiologyMt which do not have a #$denotation assertion in the #$EnglishMt. Then you could ask a query in the #$BiologyMt like so:
(and (knownSentence (genls ?FRUIT Fruit)) (istAsserted GeneralEnglishMt (denotation ??WORD ??POS ??SENSE ?FRUIT))) (#$istAsserted :MT :SENTENCE)
is equivalent to
(#$thereExists ?ASSERTION (#$thereExists ?GENLMT (#$and (#$genlMt :MT ?GENLMT) (#$assertionMt ?ASSERTION ?GENLMT) (#$assertionSentence ?ASSERTION :SENTENCE)))
See the constants
 #$assertedSentence
 #$istAsserted
 #$assertedPredicateArg
 #$assertionSentence
in the KB for more details.