Re: function terms in Euler, n3, and RDF [was: gedcom-relati

> [Jos]
> My main practical concern now is how to build an internal
> representation of this f(?x) or what kind of computational
> mechanisms should be involved?

In proto13 (fall 1999) I implemented a table of (skolem function,
bindings of its arguments, function result), which you could look up
either by (function, bindings) or (function, result).  You want the
later case in backward chaining, of course.

I was never sure I correctly handled the cases around having f(?x),
f(?x, ?y), f(?x, ?z) at the same time (during backward chaining).
Thinking about it now, I'm not sure those would ever arise from
skolemization, but my syntax let you offer them.

In proto16 (summer/fall 2000), I implemented a structure where each
rule could only be used in a backward-chaining after turning into a a
"translated rule" which knew its depth in the search tree.  I did this
just to save rule alloc/dealloc during tree searching, but it seemed
to handle the skolem problem for me.

When you descend to a new depth (making a new translated rule) you
just generate a new term in the place of any existential variables.
It doesn't address the problem of one exivar being in two different
rules, but I don't think that's a problem since my rules
allow a conjunction of triples in the conclusion.

In my logic, as you may recall, rule parts are conjoined triples:

  rule "name"  ($someone resides_in $region
                ==> 
		$someone has_a !home;     # existential variable "!home"
                !home located_in $region );

I take a rule like this as license to add as many triples as I want in
the form of the conclusion, if the premise is met.   That does not mean
I infer $someone has an infinite number of homes, just that there are
an infinite number of terms for their home or homes.  (The number of
homes is simply not information present here.)

The rule "depth" only matters when a single rule is used more than
once in a proof.  An example...  (I can't think of a recursive
example, but with my goal-list approach, I think this amounts to the
same thing.)

   rule "everone is loved by someone" ( ==> !foo loves $x );
   rule "indirect love" ( $x loves $y; $y loves $z ==> $x likes $z );
   rule "indirect like" ( $x likes $y; $y likes $z ==> $x knows $z );
   rule "output" ( $someone knows bill ==> return done done );

nile says (in a lousy old proof format, using !n for new terms)

Proof. proven: (foo!12, knows, bill)
Proof.    proven: (foo!12, likes, foo!7)
Proof.       proven: (foo!12, loves, foo!10)
Proof.          gives... (foo!12, loves, foo!10)
Proof.       proven: (foo!10, loves, foo!7)
Proof.          gives... (foo!10, loves, foo!7)
Proof.       gives... (foo!12, likes, foo!7)
Proof.    proven: (foo!7, likes, bill)
Proof.       proven: (foo!7, loves, foo!5)
Proof.          gives... (foo!7, loves, foo!5)
Proof.       proven: (foo!5, loves, bill)
Proof.          gives... (foo!5, loves, bill)
Proof.       gives... (foo!7, likes, bill)
Proof.    gives... (foo!12, knows, bill)
Proof. gives... (return, done, done)

  -- sandro

Received on Friday, 9 March 2001 11:37:49 UTC