[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