search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
243 stars 34 forks source link

Tarski's question #61

Closed LeventErkok closed 11 years ago

LeventErkok commented 11 years ago

http://en.wikipedia.org/wiki/Tarski%27s_high_school_algebra_problem

Can we use SBV/SMT to model this? Would make a nice example.

jwaldmann commented 11 years ago

you mean "what the smallest algebra for which W(x, y) is not true but the eleven axioms above are"?

this can't be too hard (in principle): encode the tables of values of plus, times and power by N x N x N booleans each (where encodef = True iff f(x,y)=z ), and function composition as composition of relations.

Cf. http://hackage.haskell.org/packages/archive/satchmo/1.9.1/doc/html/Satchmo-Relation-Op.html

It would indeed make a nice example.

LeventErkok commented 11 years ago

I was essentially thinking of just using SInteger as the underlying type, and introduce +, *, ^ as uninterpreted functions over SInteger; with the axioms given on that page. Then prove that the first example in there follows from them, and the second doesn't.

Since I have the luxury of SMT solving, I can just use true Integers and need not resort to bit-vectors. Maybe what you said is essentially the same as this.

I'd be happy to merge a pull-request if you were to go ahead and try it out in SBV!

jwaldmann commented 11 years ago

Well, you want to prove that the right-hand side of W(x,y) is not reachable from the left-hand side by rewriting steps w.r.t. the Tarski axioms. This seems hard. I don't see how a SMT solver would do this. In fact the only method I can think of is to find an invariant (w.r.t. rewriting) that holds for the lhs, but not for the rhs. A (methodically) easy way is to specify the invariant by an interpretation (an algebra). The simplest case is interpretation into a finite domain, and that's what I was suggesting. This can be encoded in a propositional formula.

In fact I just did this, https://github.com/jwaldmann/satchmo/blob/master/examples/Wilkie.hs , but this is really only a proof-of-concept thing. It creates CNFs with 1.3 mio (1.9 mio, resp.) variables for domain size 11 (12, resp.), and the number of clauses is 10 times that. I'll give minisat some hours, while thinking of a better encoding ... (I've seen case where minisat answers YES after more than one day.) I'm sure the propositional encoding could be written in SBV, modulo syntax.

LeventErkok commented 11 years ago

That's pretty cool. I'm not sure if an SMT solver can do better, given all those axioms will be quantified, and quantifier reasoning is typically problematic. The solver will probably come back and say "unknown", but I think it's worth a shot. I'll give it a try as soon as I can. It'll at least be easier to read in the SBV notation, I think.

jwaldmann commented 11 years ago

(everything is all-quantified at the outermost level, that's not too bad)

There is in fact another (direct) approach for proving that W(x,y) is independent of the Tarski Axioms: normalized completion as in http://cl-informatik.uibk.ac.at/software/mascott/ (and the papers cited there). At least that's how I understand it: compute a convergent completion C of the axioms and then check that lhs and rhs of W(x,y) have different C-normal forms. I think this is not currently a part of SMT solvers, though.

BTW, for my SAT encoding, Minisat run out of memory after 1 day. Well, it was a long shot.

LeventErkok commented 11 years ago

My naive SMT coding didn't do well either: I killed it after 30 mins, it's rather pointless to wait any longer; It's just not interesting at that point.

I still intend to play around with Z3's "tactic" engine to see if I can get a proof going, at least for the case where we know the given axioms are sufficient to do a proof of an equality. (Like the first example on the wikipedia page.) So, I'm not quite giving up on this yet, but I do agree it's a long shot even with SMT.

LeventErkok commented 11 years ago

Playing around with axioms didn't really produce anything worth pursuing. It's conceivable someone who is well-versed in Z3-tactic language can get this proof going, but it would essentially be hand-holding the SMT solver every step of the way; which is rather pointless. Real theorem-provers, such as Isabelle, ACL2, HOL are much more suitable for this sort of tasks, needless to say.

Maybe in 10 years time! when SMT solvers become really really smart!