search

ontologyportal / sumo

Suggested Upper Merged Ontology (SUMO)
227 stars 70 forks source link

Difference between `forall` and implication during inference #391

Open twitchyliquid64 opened 1 month ago

twitchyliquid64 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

Hi Tom,

  I'd recommend watching my video about inference in first order logic

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 https://github.com/ontologyportal/sumo/issues/391, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAQG6HPFDPSTZXMLL2P6QXTZYBOVTAVCNFSM6AAAAABOWVXUYWVHI2DSMVQWIX3LMV43ASLTON2WKOZSGU2DGMZYHE2TINY. You are receiving this because you are subscribed to this thread.Message ID: @.***>

twitchyliquid64 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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

twitchyliquid64 commented 1 month ago

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 commented 1 month ago

The resolution rule over CNF formulas does exactly that.