Hacker News Reader

Comment by 1ris | Hacker News Reader

This is really huge.

Maybe Idris or Coq integrate Z3.

Coq already could, if they wanted to. Z3 supports the SMT-Lib format, which means that any theorem prover that can both output that and execute a shell command can invoke Z3. This has no bearing on Z3's specific license, unless you want to use that tool for commercial purposes. For an example of this being used in a similar tool to Coq, Isabelle/HOL's 'Sledgehammer' tactic will attempt to use Z3 (and then reconstruct a proof) where its own solvers fail.

It's all pretty nifty!

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.306...

HOL4 also has Z3 (and Yices) support, but I think the Z3 support is a little out of date (in particular, it errors immediately on start).

One of the main devs of Z3, Leonardo de Moura, is acutally working on a new, dependently typed, theorem prover called "Lean": http://leanprover.github.io/

Is Lean an LCF system or Curry-Howard based? It seems to be the latter, but if so, what's it's main advantage over the many other Curry-Howard based systems?

Idris and Coq are based on the Curry-Howard correspondence. That makes it difficult / impossible to integrate Z3, because Z3 in general does not output concrete proofs. More precisely, some Z3 modules can output proof objects, but not all. There is work on integrating Z3 with LCF-style provers like Isabelle [1]. There is also active work on Z3 integration with Coq, although I'm not sure how this works. See [2] for a brief discussion of these issues by one of the Z3 authors.

[1] http://www21.in.tum.de/~boehmes/proofrec.pdf

[2] http://stackoverflow.com/questions/11531589/difference-betwe...

Are there actually cases where Z3 will say sat, but not output a model when you ask for it?

I haven't run into that issue myself, but I've mostly written toy code for it.

Models are not proofs (in fact they're the opposite). In SAT/SMT, a proof is a sequence (a tree really) of deductions that show that you can conclude "false" from the set of initial assumptions, and that, therefore, there is no model.

I'm not sure I understand what you are saying here.

The tree of resolution deductions that SAT provers (modulo theories or otherwise) like Z3 produce is of course a proof in a valid proof system. Typically that is some variant of a propositional resolution proof system. The problem is that the reasoning is classical: to show A, falsity is deduced from (not A). This is not constructively valid, you can only deduce (not not A) if (not A) implies falsity.

So the resolution proof that Z3 outputs can be converted to a classical proof and expressed in classical proof systems like (Isabelle/)HOL, but not in constructive systems like Coq and Agda.

Either I misread the parent's question or (s)he edited it. I had read it as "[...] cases where Z3 will say sat, but not output a proof when you ask for it", and was simply trying to clear up the misunderstanding that a 'sat' answer should come with a proof.

Reply on news.ycombinator.com