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

Question: Completeness of Proofs #559

Closed d4hines closed 4 years ago

d4hines commented 4 years ago

Hi! This project looks great! I'm curious though - given the supported data types, what are the limits to the completeness of automatic theorems. E.g, it's not possible to prove arbitrary proofs about the full set of Haskell functions over the integers. For what subset of Haskell over what subset of data types is sbv complete w.r.t proofs? Thanks!

LeventErkok commented 4 years ago

SBV acts as a conduit from Haskell to SMT-solvers. It can only handle a subset of Haskell, obviously. That subset is carefully chosen so that the translation should remain decidable when mapped to SMTLib. (http://smtlib.cs.uiowa.edu/) If that's what you mean by completeness, then yes: It's complete for the subset it can handle. But that's not a very usable/useful definition.

I'm not sure if this answer helps. If you have a more concrete question, feel free to elaborate.

d4hines commented 4 years ago

No, this indeed answers my questions. Thank you very much.