[Prev][Next][Index]

# (Q): Ordering formulas in LP

```Can someone please help me with my ordering problem in LP.
I have a simple lsl file that reads:

%%%%%%%%%%
Test: trait

includes Boolean

introduces

[__ , __]: E, E -> E
__ ! __ : F, E -> E
commutative: F -> Bool

asserts

\forall f: F, e, e': E

commutative (f) <=> (f ! [e, e'] = f ! [e', e]);

%%%%%%%%%%

and I am trying to generate the rewrite rule, l =

commutative (f) -> (f ! [e, e'] = f ! [e', e])

as opposed to the incorrectly (for me) ordered r =

(f ! [e, e'] = f ! [e', e]) -> commutative (f)

Every technique that I have tried has given me r instead
of l as my rewrite rule.  I have tried:

1.  Just exec'ing Test_Axioms

2.  Exec'ing Test_Axioms, and then entering

unorder Test
set ordering left-to-right
order Test

3.  First registering, as in

declare sorts F, E

declare operator
__ ! __: F, E -> E,
[__, __]: E, E -> E
commutative: F -> Bool
..

register top commutative

and then exec'ing Test_Axioms.  This leaves the
formula without orienting into a rewrite rule at all.
At this point, using technique 2 again gives me the
wrong ordering of the formula.

4.  First registering, as in

declare sorts F, E

declare operator
__ ! __: F, E -> E,
[__, __]: E, E -> E
commutative: F -> Bool
..

register height commutative > (!, [__, __], =:E, E -> Bool)

and then exec'ing Test_Axioms.  This (like 3) leaves the
formula without orienting into a rewrite rule at all.
At this point, using technique 2 again gives me the
wrong ordering of the formula.

I'm guessing that I'm going to have to use a polynomial
ordering, but I haven't been able to figure out how from
the help file.  If anyone can help, I would
be most appreciative.

- Mitch

```