Q3B : state-of-the-art QBF magic gives a radically different approach to quantified bit-vectors.
-
-
Do any of them produce viable constructive proofs of quantified statements today? Translating a model to any of those languages seems straightforward, but having seen a terrifying native Agda Presburger solver makes me doubt outside evidence of quantified stmts would really work
-
CVC4 ( Andy, Yoni and Cesare ) and veriT ( Pascal ) are the only people I know who are working on this.
End of conversation
New conversation -
-
-
CVC4 and veriT via various plug-ins. Maybe Lean in the future but remember this is only one way of rating solvers.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.