Re: Proposition about functions

Thanks Hans
What I am trying to do is reason about the axioms of group theory. What I 
have so far is:

;;; -*- Mode: Lisp; Package: STELLA; Syntax: COMMON-LISP; Base: 10 -*-

(CL:IN-PACKAGE "STELLA")

(DEFMODULE "/PL-KERNEL-KB/PL-USER/GROUP"
  :INCLUDES "PL-USER")

(IN-MODULE "/PL-KERNEL-KB/PL-USER/GROUP")

(IN-DIALECT :KIF)

(DEFCONCEPT OPERATION)

(DEFFUNCTION FOLLOWED-BY ((?A OPERATION) (?B OPERATION))
  :-> (?C OPERATION))

(DEFFUNCTION INV ((?A OPERATION))
  :-> (?B OPERATION))

(DEFRULE ASSOCIATIVITY
  (forall (?a ?b ?c)
     (<= (exists (?v29 ?v31 ?v30)
            (and (= (FOLLOWED-BY ?b ?c) ?v29)
                 (= (FOLLOWED-BY ?a ?b) ?v30)
                 (= (FOLLOWED-BY ?v30 ?c) ?v31)
                 (= (FOLLOWED-BY ?a ?v29) ?v31)))
         (and (OPERATION ?a)
              (OPERATION ?b)
              (OPERATION ?c)))))

(ASSERT (OPERATION I))

(ASSERT (forall (?a)
           (<= (exists (?v29)
                  (and (= (INV ?a) ?v29)
                       (= (FOLLOWED-BY ?a ?v29) I)))
               (OPERATION ?a))))
(ASSERT (OPERATION A))
(ASSERT (OPERATION B))
(ASSERT (OPERATION C))
(ASSERT (forall (?a)
           (<= (= (FOLLOWED-BY I ?a) ?a)
               (OPERATION ?a))))
(ASSERT (forall (?a)
           (<= (= (FOLLOWED-BY ?a I) ?a)
               (OPERATION ?a))))
(ASSERT (CLOSED FOLLOWED-BY))
(ASSERT (CLOSED INV))

Although associativity is working correctly:
(ask (= (followed-by a (followed-by b c)) (followed-by (followed-by a b) 
c)))
TRUE

and identity is working correctly:
(ask (= (followed-by a (inv a)) i))
TRUE

When I try both, the result is incorrect:
(ask (=(followed-by a (followed-by (inv a) b)) b))
FALSE

Should not the engine carry out the 2 substitutions above and answer TRUE?

Robert
-----Original Message----- 
From: Hans Chalupsky
Sent: Wednesday, July 06, 2011 1:57 AM
To: Robert Onslow
Cc: [email protected]
Subject: 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