Menu

Skolemization not working as expected?

Help
2016-08-24
2016-08-24
  • David Sekora

    David Sekora - 2016-08-24

    When I write a formula involving thereExists, Skolemization appears to happen. For example, if I have a person named TestPerson1234, and assert an encoding of the sentence "somebody loves TestPerson1234" like this:

    (thereExists ?X (loves ?X TestPerson1234))
    

    then Cyc generates a function like (SKF-5095300849) to slot into the formula. This is fine and well, and querying the exact formula "(loves (SKF-5095300849) TestPerson1234)" returns True as expected. However, when I try to ask "who loves TestPerson1234?" with the query "(loves ?X TestPerson1234)", the system is unable to find anything! I suspect this has something to do with the indeterminacy, but if anyone has any insight on this that would be great.

    That's the core issue, but here's some background/context (in case there's a better overall approach, or something wasn't clear):

    The reason I want to be able to do this is that I am trying to encode a goal system for artificial agents. There is a preexisting predicate (goals IntelligentAgent CycLSentence-Assertible), but it's not quite robust enough for what I need. So, my idea was to use a Davidsonian representation to encode various properties of goals such as weights, types, and times, like this:

    ; "Agent1234 has a goal to acquire Sandwich1"
    (thereExists ?NEWGOAL
        (and
            (isa ?NEWGOAL acquireResourceGoal)
            (targetOfGoal Sandwich1 ?NEWGOAL)
            (hasGoalObject Agent1234 ?NEWGOAL)
            (goalHasWeight ?NEWGOAL 5)))
    

    This wasn't working like I wanted it to, because again the generated Skolem function wasn't being found by inference. If this was all I wanted to do, I could just specify goal objects explicitly (e.g. create a constant 'Goal1234' and assign it properties). However, I would also like to be able to reason about related concepts, such as shared goals. This still might not seem to be a problem, since we could have a rule like:

    ; "Agents have the same goals as their friends"
    (implies
        (and
            (hasGoalObject ?AGENT1 ?GOAL)
            (friends ?AGENT1 ?AGENT2))
        (hasGoalObject ?AGENT2 ?GOAL))
    

    But, while people want to see their friends achieve their goals, it doesn't seem quite right to make them literally have the SAME goal objects - compare "I want to eat a sandwich" to "I want David to eat a sandwich". At the very least, they will likely have different weights; this could perhaps be "fixed" by just adding the weight directly to my hasGoalObject predicate, but that seems inelegant and (more importantly) doesn't generalize to other places where we want to be able to dynamically generate new goals. There are endless examples where we might want this functionality, like this:

    (forAll ?X
      (implies
        (and
            (inFrontOf-Directly ?X David)
            (isa ?X Sandwich))
        (thereExists ?EATGOAL
            (and
                (hasGoalObject David ?EATGOAL)
                (goalHasWeight ?EATGOAL 100)
                (targetOfGoal ?X ?EATGOAL)))))
    

    My current workaround is to do it "manually" - shoving all the work (of generating new goal constants and asserting things about them) to a Java program interfacing with Cyc. But, this is rather unwieldy, so again if anyone has any insight here, it would be much appreciated!

    (An interesting side note, if I later add this formula to the KB from my first example:

    (forAll ?X (not (loves ?X TestPerson1234)))
    

    a contradiction should arise, but none does! So then, of course, we can derive any silly thing we want. I'm guessing it's just too expensive to look for this kind of contradiction?)

     

    Last edit: David Sekora 2016-08-24
  • David Baxter

    David Baxter - 2016-08-24

    I think you're right about the skolem term not being returned as a binding because it is indeterminate. If you ask (thereExists ?X (loves ?X TestPerson1234)), you should get that the query was proven.

    There is an inference parameter that allows the inference engine to return indeterminate terms as bindings that you can set if you really want to get the skolem term back.

     
  • David Sekora

    David Sekora - 2016-08-24

    Oh, that's what I was missing! I just tested it out, and a query like this works to extract e.g. the weight property:

    (thereExists ?X 
      (and 
        (hasGoalObject TestPerson1234 ?X) 
        (goalHasWeight ?X ?WEIGHT)))
    

    Can't believe I didn't make the connection before - I didn't need the actual skolem term, I just needed a way to reference the properties. Thanks!

     
  • David Sekora

    David Sekora - 2016-08-24

    Of course, it's still awkward that the query (loves ?X TestPerson1234) doesn't find anything, but this is definitely workable.

     

Log in to post a comment.