Doe this count? http://svn.clifford.at/handicraft/2018/rule3smt/rule3.smt … (I hope it's correct, I just got up and am not entirely awake yet. :)
-
This Tweet is unavailable.
-
This Tweet is unavailable.
-
This Tweet is unavailable.
tbh I'm not even sure what "putting the induction in the SMT proof" would look like. I've always just created individual proofs for base case and induction step. (Base case is just P=0 in my code. So it's just one proof for base case and induction step.)
-
-
Given that recursive functions are A. pretty new and B. kind of just syntactic sugar, I doubt anyone is computing inductive proofs with them. CVC4 does attempt induction for quantifiers plus there is the "Horn Clause" stuff but those aren't for define-fun-rec.
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.