Difference between forall and implication during inference

[twitchyliquid64]

Hiya, love the project!

I'm working on inference over SUMO for fun and learning. I (eventually) found the spec for the format here, but I'm afraid im having trouble understanding some of the rule operators.

Implication/bi-implication seem easy enough to implement, I just search the knowledgebase for variables for each value which make the predicates true, and then create new entries in the knowledgebase based on the implication and those variable values.

I'm having trouble understanding forall however. The document gives this example for "All farmers like tractors":

(forall (?F ?T)
 (=>
   (and
     (instance ?F Farmer)
     (instance ?T Tractor))
   (likes ?F ?T)))

How is this different to implication? Wouldn't I end up with the same info in the knowledgebase by just doing:

(=>
  (and
    (instance ?F Farmer)
    (instance ?T Tractor))
  (likes ?F ?T)))

Maybe the difference is just intent and not relevant for inference, in which case I don't understand when I would use forall vs implication.

Thanks!
Tom

[arademaker]

In SUO-KIF, variables that were not explicit instantiated are assumed to be universally instantiated. So the two formulas are equivalent. Just the second is a simplied version of the first without the explicit quantifier. Any tool reading the SUO-KIF file need to fill the gaps and add the implicit universal quantifier in all formulas were any free variable can be found.

[apease]

Hi Tom,   I'd recommend watching my video about inference in first order logic - https://youtu.be/J3Pm43O48Uo?si=RQVo-kAR-hd2zcU_  as well as possibly doing my course on SUMO overall https://www.ontologyportal.org/course.html .  In the formulas below, the universal quantifier is not required, since unquantified variables are implicitly universally quantified in the outermost scope. all the best, Adam

…

On 9/23/24 11:45 AM, Tom wrote: Hiya, love the project! I'm working on inference over SUMO for fun and learning. I (eventually) found the spec for the format here <http://ontolog-archives.cim3.net/file/resource/reference/SIGMA-kee/suo-kif.pdf>, but I'm afraid im having trouble understanding some of the rule operators. Implication/bi-implication seem easy enough to implement, I just search the knowledgebase for variables for each value which make the predicates true, and then create new entries in the knowledgebase based on the implication and those variable values. I'm having trouble understanding |forall| however. The document gives this example for "All farmers like tractors": |(forall (?F ?T) (=> (and (instance ?F Farmer) (instance ?T Tractor)) (likes ?F ?T))) | How is this different to implication? Wouldn't I end up with the same info in the knowledgebase by just doing: |(=> (and (instance ?F Farmer) (instance ?T Tractor)) (likes ?F ?T))) | Maybe the difference is just intent and not relevant for inference, in which case I don't understand when I would use |forall| vs implication. Thanks! Tom — Reply to this email directly, view it on GitHub <#391>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAQG6HPFDPSTZXMLL2P6QXTZYBOVTAVCNFSM6AAAAABOWVXUYWVHI2DSMVQWIX3LMV43ASLTON2WKOZSGU2DGMZYHE2TINY>. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[twitchyliquid64]

Thanks Adam & Alexander!

That makes sense R.E implicit quantification.

I’ve skimmed those YouTube videos, I’ll be sure to take a better look.

Last question while I’m here: I understand the ‘exists’ operator is existential quantification, but in the context of inference is the engine meant to create missing concepts if such a concept doesn’t exist? (As opposed to implications that seem to create relations that don’t exist but never create concepts themselves).

[apease]

I think a better way to say this is that an existentially quantified variable denotes a constant term. If I say every horse has a head (=> (instance ?H Horse) (and (instance ?X Head) (part ?X ?H))) I've made a general statement that otherwise would have required explicitly saying "Bessie is a horse and BessiesHead is a part of Bessie", "Secretariat is a horse..." etc. I've made a general statement that doesn't require proliferating named terms such as BessiesHead. I'm not sure what you mean about implications. Any implication is a relationship among all the constant terms that appear within it. If you use a logic beyond first order, as we do with SUMO, you do have the possibility of writing formulas in which an existential quantified variables denotes a relation as in "If John and Stan are 'kin' then there exists a relation between them that is an instance of 'familyRelation'"

[twitchyliquid64]

Gotcha thanks! A combination of staring at the code I wrote and watching a bunch more of your videos made it clear.

For my question, the thing that I had missed was that relationships (I think yall call them 'functional terms') themselves are just concepts without a name, so an implication in the context of SUMO implication creating a relation is absolutely creating a concept.

The idea that implication is CNF-equivalent (=> a b is the same as or (not a) b) still breaks my brain if i try and think about it outside of the context of unification/search, but hopefully it will get clearer over time.

I have another question about relations in SUMO, but i'll stay on topic and open a different issue.

Thanks again!!

[apease]

Hi Tom, a truth table may help - two truth tables that have all the same values are logically equivalent. Even if your intuitions haven't sync'ed up, at least you have proven when two formulas are the same, and that's the case for a->b <-> -a v b

[twitchyliquid64]

I see how they are equivalent in the context of resolving a sentence to some truth value, but I don't see how the CNF form represents the the modus-ponens knowledge-creation of an implication a; if a then b; therefore b. Or maybe I am conflating two different things.

[apease]

if you have a and ~a v b then b must be true - same as modus ponens

[twitchyliquid64]

Could it be that simple? Any or (not a) b is just an implication in the domain of discourse? During inference/search I can just rewrite that to implication and (if true) keep following that path?

[apease]

The resolution rule over CNF formulas does exactly that.