# Just Launched: You can now import projects and releases from Google Code onto SourceForge

We are excited to release new functionality to enable a 1-click import from Google Code onto the Allura platform on SourceForge. You can import tickets, wikis, source, releases, and more with a few simple steps.

## Mathematical operators in Cyc

peepal
2004-12-08
2013-05-28

• peepal
2004-12-08

hi all,
I am trying to write a microtheory, in which I want to use few objects from a databank (these objects may have references like 1234 or any digit or String or combination of both). Now I want to use the mathematical operators in my microtheory. Is it possible to check for equal(==) operation like ( Is 3 equal to 4) etc in Cyc without having to feed the information that 3 is indeed not equal to 4. Can cyc determine on its own if two digits are equal or not?

peepal

• Yeb Havinga
2004-12-08

EL Query :
(not
(equals 3 4))

Query was proven True *[Explain]

• Hash Dollar
2004-12-21

#\$different works as well:

> Mt : UniversalVocabularyMt
> EL Query :
> (different 3 4)
>
> Status : Suspended, Exhaust Total
>
> Query was proven True

#\$

• Yeb Havinga
2004-12-22

Can Cyc prove that <> is the same as !=?

(#\$forAll ?X
(#\$forAll ?Y
(#\$equiv
(#\$not
(#\$equals ?X ?Y))
(#\$different ?X ?Y))))

• Hash Dollar
2004-12-22

Yeb,

Note that #\$equiv is an #\$ELRelation with the following #\$expansion

> Mt : BaseKB
> (expansion equiv
>        (and
>            (implies :ARG1 :ARG2)
>            (implies :ARG2 :ARG1)))

So your query is first converted to

(and
(implies
(different ?X ?Y)
(not (equals ?X ?Y)))
(implies
(not (equals ?X ?Y))
(different ?X ?Y)))

and this query is the one that gets asked. Now, the Cyc canonicalizer converts the above into the HL form

> (or
>    (ist UniversalVocabularyMt
>        (and
>            (not
>                (equals ?var0 ?var1))
>            (different ?var0 ?var1)))
>    (ist UniversalVocabularyMt
>        (and
>            (not
>                (different ?var0 ?var1))
>            (equals ?var0 ?var1))))

and this is the query that's actually evaluated by the inference engine. The problem is, that instead of applying universal generalization, it tries to find bindings in the KB for ?var0 and ?var1, which fails. (This should probably be recoginzed by Cyc as a tautology, since any bindings for ?var0 and ?var1 in the universe of discourse would satisfy the query.)

The following two queries do work, however, because Cyc does correctly apply universal generalization when asked a direct implication (i.e. when the query formula has #\$implies in the arg0)

> Mt : UniversalVocabularyMt
> EL Query :
> (implies
>    (different ?X ?Y)
>    (not
>        (equals ?X ?Y)))
>
> Status : Suspended, Exhaust Total
>
> Query was proven True *[Explain]

and

> Mt : UniversalVocabularyMt
> EL Query :
> (implies
>    (not
>        (equals ?X ?Y))
>    (different ?X ?Y))
>
> Status : Suspended, Exhaust Total
>
> Query was proven True *[Explain]

I'm not quite sure why universal generalization doesn't apply to the (and (implies ...) (implies ...)) form, but I will try to find out.

#\$