4 ms·

How would a therom prover like z3 handle this, out of interest? Isn't it the ideal domain for it?

by orf 9y ago

justinpombrio 9y ago
It might be useful to find solutions in the first place. This article was about defining when two expressions are "essentially the same", though, and Z3 isn't going to help you construct a definition :-).
taejo 9y ago
I think the difficulty is in defining the relation, rather than proving it. The problems are so small that it probably doesn't matter how you actually prove equivalence, once you've defined it.
cwzwarich 9y ago
This isn't really an interesting question from the point of view of automated reasoning. The obvious canonical form for such an expression (with variables) is to represent it as a polynomial or rational polynomial, and I don't see why you'd ever do something like what the author of this blog post is doing.
ZephyrP 9y ago
Solving the problem of "recognizing when two arithmetic expressions are equivalent" is indeed ideal for an approach like Prolog or a SAT/SMT solver. In fact SMTLIB2 has a standardized expression for asserting if two expressions are identical. Conversely, many APIs make testing that sort of claim easy (and even emjoy tactics for things like synthesize new expressions w/ respect to some 'cost' function for each sub-expression, etc) With that said, the author of this article seems to be interested in some sort of other question entirely.
wsxcde 9y ago
Z3 and similar tools use a combination of canonicalization followed by brute force search. The canonicalization uses techniques similar to what the OP describes. (+ a (+ b c)) and (+ c (+ b a)) are both rewritten as (+ a b c). These rewrites rely on pattern matching. At this point, if the query is syntactically solvable, we are done. Often queries are not, so the solver uses a symbolic decision procedure. The specific decision procedure depends on the formula. For example, Linear Integer Arithmetic (which allows addition of variables and multiplication by only constants) can be solved using Simplex.

How would a therom prover like z3 handle this, out of interest? Isn't it the ideal domain for it?

by orf 9y ago

How would a therom prover like z3 handle this, out of interest? Isn't it the ideal domain for it?

It might be useful to find solutions in the first place. This article was about defining when two expressions are "essentially the same", though, and Z3 isn't going to help you construct a definition :-).

taejo 9y ago

I think the difficulty is in defining the relation, rather than proving it. The problems are so small that it probably doesn't matter how you actually prove equivalence, once you've defined it.

cwzwarich 9y ago

This isn't really an interesting question from the point of view of automated reasoning. The obvious canonical form for such an expression (with variables) is to represent it as a polynomial or rational polynomial, and I don't see why you'd ever do something like what the author of this blog post is doing.

ZephyrP 9y ago

Solving the problem of "recognizing when two arithmetic expressions are equivalent" is indeed ideal for an approach like Prolog or a SAT/SMT solver. In fact SMTLIB2 has a standardized expression for asserting if two expressions are identical. Conversely, many APIs make testing that sort of claim easy (and even emjoy tactics for things like synthesize new expressions w/ respect to some 'cost' function for each sub-expression, etc) With that said, the author of this article seems to be interested in some sort of other question entirely.

wsxcde 9y ago

Z3 and similar tools use a combination of canonicalization followed by brute force search. The canonicalization uses techniques similar to what the OP describes. (+ a (+ b c)) and (+ c (+ b a)) are both rewritten as (+ a b c). These rewrites rely on pattern matching. At this point, if the query is syntactically solvable, we are done. Often queries are not, so the solver uses a symbolic decision procedure. The specific decision procedure depends on the formula. For example, Linear Integer Arithmetic (which allows addition of variables and multiplication by only constants) can be solved using Simplex.