Re: Proposition about functions

I am not completely sure what you are trying to do, but here is my best guess:

I assume, you wanted "followed-by" to be a function of two input arguments ?a
and ?b and the output argument ?c.  To do that you need to use the value arrow
:-> instead of the :=> arrow which means logical implication:

    (deffunction followed-by (?a ?b) :-> ?c)

Alternatively, you could have defined the function simply like this:

    (deffunction followed-by (?a ?b ?c))

Then, to specify the associativity of "followed-by", you could use the
following rule:

(defproposition associativity 
  (forall (?a ?b ?c ?v) 
    (<=> (followed-by ?a (followed-by ?b ?c) ?v)
         (followed-by (followed-by ?a ?b) ?c ?v))))

However, PowerLoom wouldn't really be able to do any reasoning with the
resulting rules, since the function terms introduce existentials on both sides
of the implication which currently won't get skolemized away properly.

An alternative formulation that PowerLoom can use are the following two rules:

(defproposition associativity-ab
  (forall (?a ?b ?c ?ab ?bc ?v) 
    (=>  (and (followed-by ?a ?b ?ab)
              (followed-by ?b ?c ?bc)
              (followed-by ?a ?bc ?v))
         (followed-by ?ab ?c ?v))))

(defproposition associativity-bc
  (forall (?a ?b ?c ?ab ?bc ?v)
    (=>  (and (followed-by ?a ?b ?ab)
              (followed-by ?b ?c ?bc)
              (followed-by ?ab ?c ?v))
         (followed-by ?a ?bc ?v))))

If you want to specify associativity for more than one binary function, you
could define the following meta-property which would define the rules
automatically during forward inference:

(defrelation associative (?r)
  :=>> (forall (?a ?b ?c ?ab ?bc ?v) 
         (=>  (and (holds ?r ?a ?b ?ab)
                   (holds ?r ?b ?c ?bc)
                   (holds ?r ?a ?bc ?v))
              (holds ?r ?ab ?c ?v)))
  :=>> (forall (?a ?b ?c ?ab ?bc ?v) 
         (=>  (and (holds ?r ?a ?b ?ab)
                   (holds ?r ?b ?c ?bc)
                   (holds ?r ?ab ?c ?v))
              (holds ?r ?a ?bc ?v))))

The you can define your associative function like this:

(deffunction followed-by (?a ?b ?c)
   :associative true)

Hans

>>>>> Robert Onslow <[email protected]> writes:

> Dear All
> Is it possible to have a proposition about a function:

> (deffunction followed-by (?a ?b) :=> ?c)

> (defproposition associativity (forall (?a ?b ?c) (=> (<=> (followed-by ?a 
> (followed-by ?b ?c)) (followed-by (followed-by ?a ?b) ?c))))

> Robert Onslow

> _______________________________________________
> powerloom-forum mailing list
> [email protected]
> http://mailman.isi.edu/mailman/listinfo/powerloom-forum