mi9p8
2010-06-29
Hello, I am new to redlog/reduce system. I have a question about simplification.
I input a mathematically identical statement in two different representations as shown below. Obviously the Output2 is redundant. How do I get the redundancy removed? rlsimpl or other simplification functions did not work.
Statement: For all (x,y), if a point (x,y) is in a (a*b) rectangular area, that point is in a circle of radius, r.
Input1: rlqe(all({x,y}, x^2 < a^2 and y^2 < b^2 impl x^2 + y^2 < r^2), {a>0, b>0, r>0});
Output1: a^2+b^2-r^2 <= 0
Input2: rlqe(all({x,y}, -a < x and x < a and -b < y and y < b impl x^2 + y^2 < r^2), {a>0, b>0, r>0});
Output2: a^2+b^2-r^2 <= 0 and (a+r <= 0 or a-r <= 0) and (a^2+b^2-r^2 < 0 or b^2-r^2 > 0 or (b+r <> 0 and b-r <> 0))
Another example:
Input3: rlsimpl(x^2 < a^2 and (-a < x and x < a), {a < 0});
Output3: a^2 - x^2 > 0 and a+x>0 and a-x > 0
This Input3 did not work as I expected. I tried Groebner and Tableau as well with the same result. I expected my output to be either "a^2 - x^2 > 0" alone or "a+x>0 and a-x > 0". Apparently I was wrong. Am I misunderstanding something?
Thanks.
Thomas Sturm
2010-07-07
Simplification is heuristic and does not provide any canonical or minimal forms. There is a trade-off between quality and efficiency so that the used methods should be general, efficient, and applicable to general input with high probability.
Some details can be found here:
Simplification of quantifier-free formulae over ordered fields. Journal of Symbolic Computation, 24(2):209-231, August 1997.
Note that for small formulas with few variables, rlcad also yields good simplification in some cases. It does not work for your example though.
Thomas
mi9p8
2010-07-07
Thomas,
Thank you for your reply. I am going to read the paper.
I have another question.
When I copy the formula that appears in reduce, and paste it in a text editor, I get HTML code. Is there any way I can get it copied as simple text without HTML tags?
Thank you
Arthur Norman
2010-07-07
> When I copy the formula that appears in reduce, and paste it in a text editor, I get HTML code.
> Is there any way I can get it copied as simple text without HTML tags?
With the CSL version that is my fault. When I introduced coloured prompts etc I wanted cut and paste from Reduce back into Reduce to copy eg your input text without any embedded prompts, and I achieved that by putting it on the clipboad in HTML. In "fancy" mode I do not have code that copies displayed formulae (yet???)
It probably needs a "copy as plain text" option, but I go away on holiday rather soon so I will not put that in right now.
The easiest way I can suggest as a work-around is to run it as
bin/redcsl -w
to run it in console mode rather than windowed mode, than the coy and paste pacilities become the one that your terminal supports and that is not liable to mess with HTML for you!
Arthur
mi9p8
2010-07-07
That works for me. "copy as plain text" option would be great.
Thank you.
Arthur Norman
2010-07-07
The subversion has an attempt at "Copy Text". You need to recomile the FOX library to get it. Easiest is to delete the whole cslbuild directory and reconfigure and build again fron scratch, I suspect. I hope it works!