test cases for unfailing KBC with conditional simp rules

Stream: general

[Jared green]

I am trying to build an implementation of Knuth-Bendix completion for conditional rewrites with unconditional unoriented equations. I need to test it. Does anyone know of such rewrite systems with a terminating, confluent(to equivalence on unoriented equations) completion?

[Frederick Pu]

Heq?

[Jared green]

i dont think so. im talking about a actual set of equations and conditional rewrite rules. i need to provide them individually and explicitly.

[Frederick Pu]

what about the word problem for commutative groups?

[Frederick Pu]

and the reduction ordering is just how many terms u have in the word
for example abca^-1 < abcdaa

[Jared green]

i need conditional rewrites. where the conditions are equations.

[Jared green]

and the completion would have to be longer than the initial set or its not very useful for testing.

[Frederick Pu]

word problem on real numbers, you need the nonzero condition in order to cancel multiplicative inverses

[Jared green]

surely not the full real numbers right? because that doesnt have decidable equality.

[Jared green]

also inequations are not supported.

[Shreyas Srinivas]

Check out the equational theories project

[Jared green]

anything in particular you have in mind?

[Jared green]

as far as i know all the equations tested in the equational theories project have been unconditional. so like, are you telling me to add this to that project or what?